| Age | Commit message (Expand) | Author |
|---|
| 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-03-31 | Add documentation on the treatment of [if] and [let (x1, ... xn) := ..] | msozeau |
| 2010-03-30 | 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-29 | Several bug-fixes and improvements of coqdoc | herbelin |
| 2010-03-28 | 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-27 | 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-24 | Fixed bug #2260 (check of resolution of all evars in the declaration | herbelin |
| 2010-03-23 | 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-19 | 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-18 | 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-15 | 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-12 | 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-11 | 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-10 | 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-08 | Consider OccurCheck a catchable exception. | msozeau |
| 2010-03-08 | Application des patches envoyés par F. Besson pour micromega | notin |
| 2010-03-07 | Reorder resolution of type class and unification constraints. | msozeau |
| 2010-03-07 | Fix lifting of constraints in generalized rewriting tactic. | msozeau |
| 2010-03-07 | Fix treatment of remaining unification constraints: raise a more | msozeau |
| 2010-03-06 | Fixes in rewrite and a Elimination/Case to Scheme: | msozeau |
| 2010-03-06 | Adding Function as keyword for coqdoc | thery |
