| Age | Commit message (Expand) | Author |
|---|
| 2012-11-25 | Monomorphization (tactics) | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-10-04 | Revert r15851 "En cours pour bug 2836". | herbelin |
| 2012-10-04 | En cours pour bug 2836 | herbelin |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-18 | Cleaning interface of Util. | ppedrot |
| 2012-09-17 | More cleaning on Utils and CList. Some parts of the code being | ppedrot |
| 2012-09-15 | Some documentation and cleaning of CList and Util interfaces. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-17 | Added a flag to control the use of typing when instantiating applied | herbelin |
| 2011-11-24 | Added a DEPRECATED flag in declaration of options. For now only two options a... | ppedrot |
| 2011-10-22 | Fixing Equality.injectable which did not detect an equality without | herbelin |
| 2011-10-11 | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin |
| 2011-10-11 | Various simplifications about constant_of_delta and mind_of_delta | letouzey |
| 2011-07-29 | Equality: generic equality on constr replaced by eq_constr | puech |
| 2011-07-29 | Equality: generic equality on constr replaced by eq_constr | puech |
| 2011-07-18 | Fixed a "feature" of "inversion" and "dependent rewrite" revealed by | herbelin |
| 2011-07-16 | Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and... | herbelin |
| 2011-06-18 | Relaxed the constraint introduced in r14190 that froze the existing | herbelin |
| 2011-06-18 | Generalizing flag use_evars_pattern_unification into a flag | herbelin |
| 2011-06-13 | A few comments and a dev file to summarize issues with unification | herbelin |
| 2011-06-13 | Added a flag to restrict conversion in tactic unification on the | herbelin |
| 2011-06-12 | Added a new flag for freezing evars in tactic unification. Used this | herbelin |
| 2011-06-10 | Moved allow_K to a unification flag | herbelin |
| 2011-05-26 | Fixing discriminate for identity. | herbelin |
| 2011-04-18 | Add a flag to control betaiota reduction during unification to maintain backw... | msozeau |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-03-05 | Fixing injection bug #2493 (regression introduced by fixing injection | herbelin |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-11-07 | Delayed the evar normalization in error messages to the last minute | herbelin |
| 2010-10-27 | correction of bug #2414 (report of r 13586) | jforest |
| 2010-09-20 | Added eta-expansion in kernel, type inference and tactic unification, | herbelin |
| 2010-09-17 | In the computation of missing arguments for apply, accept that the | herbelin |
| 2010-09-13 | Fix unescaped end-of-lines (OCaml warning 29) | glondu |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-29 | New pass on inductive schemes | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-05 | Improving compatibility between 8.2 and 8.3 | herbelin |
| 2010-03-27 | Applied greenrd's patch to fix bug 2255 (injection failed to | herbelin |
| 2009-12-28 | Safer, though ad hoc, approach to re-interpretation of the argument of | herbelin |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-12-14 | Improved strategy for rewriting lemma possibly depending because of evars. | herbelin |
| 2009-12-13 | Made the side-conditions of lemmas always come last when chaining "apply in" | herbelin |
