| Age | Commit message (Expand) | Author |
|---|
| 2012-11-26 | Removed some FIXME related to equality on universes. | ppedrot |
| 2012-11-26 | Small cleaning of interface in Univ | ppedrot |
| 2012-11-22 | Monomorphization (pretyping) | ppedrot |
| 2012-11-20 | Cleaning and small optimization in CList. | ppedrot |
| 2012-11-03 | Reversed roles of undefined/defined evars in Evd, thus saving precious | ppedrot |
| 2012-10-29 | Removed many calls to OCaml generic equality. This was done by | ppedrot |
| 2012-10-17 | univ inconsistency error message gives evidence of a cycle | barras |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 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 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-03-22 | Univ: enforce_leq instead of enforce_geq for more uniformity | letouzey |
| 2012-03-20 | Generalized the use of evar candidates in type inference unification: | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-17 | Added ability to take the type of applied metas into account when | herbelin |
| 2011-12-16 | Introducing a notion of evar candidates to be used when an evar is | herbelin |
| 2011-10-26 | When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty | letouzey |
| 2011-10-25 | Continuing r14585 (ill-typed restriction bug). | herbelin |
| 2011-10-22 | Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global... | herbelin |
| 2011-10-11 | More on r14536 (an unused pattern-matching remained in the commit). | herbelin |
| 2011-10-10 | Little code simplification of instantiate_evar in evd.ml | herbelin |
| 2011-10-10 | Added information about evar origin in pretty-printing evd for debug | herbelin |
| 2011-10-10 | Passed conv_algo to evar_define and move call to solve_refl to | herbelin |
| 2011-08-02 | More robust evar_map debugging printer | herbelin |
| 2011-06-21 | Cleaning debugging printer relative to new proof engine. In | herbelin |
| 2011-06-12 | Added a new flag for freezing evars in tactic unification. Used this | herbelin |
| 2011-05-13 | A better procedure for checking presence of undefined evars. | aspiwack |
| 2011-05-04 | First phase removing obsolete support for eta up to conversion in | herbelin |
| 2011-03-23 | - Remove useless grammar rule | msozeau |
| 2011-03-11 | Tentative to make unification check types at every instanciation of an | msozeau |
| 2011-03-11 | - Better error messages taking unif. constraints into account. | msozeau |
| 2011-03-10 | Forgot a use of evars_reset_evd in nf_evars, add an optional argument as | msozeau |
| 2011-03-10 | Do not forget conv_pbs when resetting an evm: | msozeau |
| 2011-02-17 | - Use transparency information all the way through unification and | msozeau |
| 2010-12-15 | Misc improvements about evar_map | letouzey |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | Added Chung-Kil Hur's smart "pattern" tactic (h_resolve). | herbelin |
| 2010-06-12 | Fixed bug #2135 (second-order unification was raising cryptic message) | herbelin |
| 2010-05-13 | Improved the efficiency of evars traverals thanks to a split of | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-03-15 | Stop dropping evar constraints when building a new goal evar defs. | msozeau |
| 2009-12-24 | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin |
| 2009-12-22 | Attached evar source to the evar_info and add location to tclWITHHOLES errors | herbelin |
| 2009-12-21 | In "progress", extending the set of evars w/o solving an existing one is | herbelin |
