Commits

Branch selector

 trunk

User selector

herbelin

Datepicker

All time

Commit History

Commits on Jun 16, 2015

• Fix by Enrico on CoqIDE not locating errors anymore since 550da87.

  herbelin

  committed
  b831c43

• Granting, undocumentedly, parsing of "Conjectures" as a synonym of

  Show description for 902032b
  herbelin

  committed
  902032b

Commits on May 22, 2015

• Continuing 4b5af0d and 69941d4 about filename case check on MacOS X.

  Show description for e7043ee
  herbelin

  committed
  e7043ee

Commits on May 20, 2015

• Answering report coq#4241 (formatting of boxes not behaving regularly

  Show description for 8241460
  herbelin

  committed
  8241460

• Continuing incomplete 4b5af0d (on MacOS X, ensuring that files

  Show description for 69941d4
  herbelin

  committed
  69941d4

Commits on May 18, 2015

• Removing option -no-native-compiler from test coq#3539 since this option is now

  Show description for ab791c6
  herbelin

  committed
  ab791c6

Commits on May 15, 2015

• Removing option -no-native-compiler from test coq#3539 since this option is now

  Show description for cd6e868
  herbelin

  committed
  cd6e868

• On MacOS X, ensuring that files found in the file system have the

  Show description for 4b5af0d
  herbelin

  committed
  4b5af0d

• Turning "Set Regular Subst Tactic" on by default (for 8.6).

  herbelin

  committed
  8aebd0c

• Merge v8.5 into trunk

  Show description for 5d015ae
  herbelin

  committed
  5d015ae

Commits on May 14, 2015

• coq#3953 now closed.

  herbelin

  committed
  76c3b40

Commits on May 13, 2015

• Documenting Set Regular Subst Tactic (though unsure this is worth the

  Show description for c5d9f48
  herbelin

  committed
  c5d9f48

• Better fixing coq#4198 such that the term to match is looked for before

  Show description for 574b409
  herbelin

  committed
  574b409

Commits on May 9, 2015

• Adjusting test-suite after 5cbc018 (subst as in 8.4 by default).

  herbelin

  committed
  39a67d5

• Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for

  Show description for 5cbc018
  herbelin

  committed
  5cbc018

• Tentatively setting cons and Some with 1st implicit argument maximal

  Show description for 290ad7c
  herbelin

  committed
  290ad7c

Commits on May 8, 2015

• A more user-friendly naming of variables of ltac names defined by

  Show description for 3bcfff9
  herbelin

  committed
  3bcfff9

Commits on May 6, 2015

• Fixing treatment of recursive equations damaged by 857e82b.

  Show description for 32a9a4e
  herbelin

  committed
  32a9a4e

• Fixing "subst" to respect v8.4 most-ancient to most-recent hyps order

  Show description for 5a0d339
  herbelin

  committed
  5a0d339

Commits on May 5, 2015

• Compatibility ocaml 3.12.

  herbelin

  committed
  a72b7db

Commits on May 1, 2015

• Fixing computation of implicit arguments by position in fixpoints (coq#4217).

  herbelin

  committed
  f19d0c7

• Giving to "subst" a more natural semantic (fixing coq#4214) by using all

  Show description for 857e82b
  herbelin

  committed
  857e82b

Commits on Apr 22, 2015

• Fixing non exhaustive pattern-matching.

  herbelin

  committed
  db29432

• Test for coq#4198 (appcontext in return clause of match).

  herbelin

  committed
  3d2cf9f

Commits on Apr 21, 2015

• Fixing coq#4198 (looking for subterms also in the return clause of match).

  Show description for a45bd59
  herbelin

  committed
  a45bd59

• Fixing coq#3383 (a "return" clause without an "in" clause is not enough

  Show description for 9fa7f38
  herbelin

  committed
  9fa7f38

• Fixing coq#3376 and coq#4191 (wrong index of maximally-inserted implicit argument

  Show description for 7d261ef
  herbelin

  committed
  7d261ef

• Some dead code.

  herbelin

  committed
  ce6bbd0

Commits on Apr 20, 2015

• Inlining "fun" and "forall" tokens in parser, so that alternative notations for

  Show description for b846c41
  herbelin

  committed
  b846c41

Commits on Apr 17, 2015

• Extra fix to 9347618 and f4ee7ee on optimizing Import of several

  Show description for 1c0a1db
  herbelin

  committed
  1c0a1db

• Fixing a few typos + some uniformization of writing in doc.

  herbelin

  committed
  ec462f7

Commits on Apr 1, 2015

• Accomodating coq#4166 (providing "Require Import OmegaTactic" as a

  Show description for 8581e1a
  herbelin

  committed
  8581e1a

• Fixing a few typos + some uniformization of writing in doc.

  herbelin

  committed
  226bf47

Commits on Mar 25, 2015

• Fully fixing bug coq#3491 (anomaly when building _rect scheme in the

  Show description for c172963
  herbelin

  committed
  c172963

• Another example about the consequence of a wrong computation of the

  Show description for 1a519fc
  herbelin

  committed
  1a519fc

Pagination

PreviousNext