| Commit message (Expand) | Author | Age |
* | Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which | herbelin | 2010-04-07 |
* | New model for user-driven translation of tokens in coqdoc | herbelin | 2010-04-06 |
* | Improving compatibility between 8.2 and 8.3 | herbelin | 2010-04-05 |
* | Fix configure script: natdynlink works without a hack on 10.6.3. | msozeau | 2010-04-05 |
* | Added a function in typing.ml to solve evars of a constr w/o going back down ... | herbelin | 2010-04-05 |
* | Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflit | aspiwack | 2010-04-05 |
* | Granting wish #2251 (forbidding rewriting a term reduced to an evar) | herbelin | 2010-04-05 |
* | Tests for bug report #2244 (pattern-unification with abstraction over Meta's) | herbelin | 2010-04-05 |
* | Partial fix to bug #2244 (ensure that pattern unification does not | herbelin | 2010-04-05 |
* | Add documentation on the treatment of [if] and [let (x1, ... xn) := ..] | msozeau | 2010-03-31 |
* | Small things about coqdoc + fixing lettuple.v test (part of bug #2289) | herbelin | 2010-03-30 |
* | Removed hard-wiring of latin1 letters in coqdoc (see bug #2275) | herbelin | 2010-03-30 |
* | Small improvements around coqdoc (including fix for bug #2288) | herbelin | 2010-03-30 |
* | Fixed small bugs introduced in commit 12890 (bug #2286, that comes | herbelin | 2010-03-30 |
* | Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using i... | letouzey | 2010-03-30 |
* | Improving error messages in the presence of utf-8 characters | herbelin | 2010-03-30 |
* | Several bug-fixes and improvements of coqdoc | herbelin | 2010-03-29 |
* | Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphic | herbelin | 2010-03-28 |
* | Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt) | herbelin | 2010-03-28 |
* | Fixing bug #2279 (printing nested let-in was in exponential time) | herbelin | 2010-03-27 |
* | Applied greenrd's patch to fix bug 2255 (injection failed to | herbelin | 2010-03-27 |
* | Fixed bug #2260 (check of resolution of all evars in the declaration | herbelin | 2010-03-24 |
* | Updated CHANGES wrt 8.3 | herbelin | 2010-03-23 |
* | Added automatic expansion on the left of recursive notations | herbelin | 2010-03-23 |
* | Changing types to reflect futur separation between toplevel and ide. | vgross | 2010-03-23 |
* | infrastructure for safe marshal-based IPC | vgross | 2010-03-23 |
* | Goal generation deported into ide/coq.ml, single function to obtain | vgross | 2010-03-23 |
* | New functions for goals fetching. | vgross | 2010-03-23 |
* | Fix bug in backtracking. | vgross | 2010-03-23 |
* | debugging | vgross | 2010-03-23 |
* | Removing unexpected printing of debug output (see bug report #2271). | herbelin | 2010-03-19 |
* | Définition de GRAMMARCMA: parsing/grammar.cma n'était plus installé, ce qu... | notin | 2010-03-19 |
* | kills a warning about vo in checker/safe_typing | letouzey | 2010-03-18 |
* | Makefile.build: (slightly) more robust sed invocation for parsing camlp4deps/... | letouzey | 2010-03-18 |
* | Myocamlbuild: slight simplification of code for .ml4 | letouzey | 2010-03-18 |
* | Oops, don't use zeta by default. | msozeau | 2010-03-15 |
* | Stop dropping evar constraints when building a new goal evar defs. | msozeau | 2010-03-15 |
* | Fix splitting evars tactics and stop dropping evar constraints when | msozeau | 2010-03-15 |
* | fixed minor pbs with test cases | barras | 2010-03-12 |
* | fixed confusion between number of cstr arguments and number of pattern variab... | barras | 2010-03-12 |
* | introduced lazy computation of size info in the guard condition | barras | 2010-03-11 |
* | Update manual on search commands | puech | 2010-03-11 |
* | Minimal test suite for search commands | puech | 2010-03-11 |
* | fix [Search] when the result has no hypothesis & constant comparison | puech | 2010-03-11 |
* | No delta-reduction in libtypes anymore | puech | 2010-03-11 |
* | Filter out "_subproof" objects from search results | puech | 2010-03-11 |
* | NMake: remove useless tactics abstract_pair, nicer comments | letouzey | 2010-03-10 |
* | NMake: Reorganization, interface for NMake_gen, explicit View, tactic destr_t... | letouzey | 2010-03-10 |
* | NMake_gen.ml: robustness w.r.t size, remove old commented stuff about shiftl | letouzey | 2010-03-10 |
* | Consider OccurCheck a catchable exception. | msozeau | 2010-03-08 |