| Age | Commit message (Expand) | Author |
|---|
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-09-10 | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin |
| 2014-05-06 | Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2014-03-26 | Moving some tactic code to the new engine. | Pierre-Marie Pédrot |
| 2014-03-01 | Fixing pervasive comparisons | Pierre-Marie Pédrot |
| 2013-10-29 | Do not generate useless argument arrays in whd_* functions. | ppedrot |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
| 2013-09-25 | Removing useless evar-related stuff. | ppedrot |
| 2013-06-04 | Backtrack on unneeded change of interface for pose_metas_as_evars. | msozeau |
| 2013-06-04 | Start documenting new [rewrite_strat] tactic that applies rewriting | msozeau |
| 2013-05-03 | Removing a redundant function from Evd. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-02-17 | Added propagation of evars unification failure reasons for better | herbelin |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-11-25 | Monomorphization (proof) | 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-07-20 | Reductionops refactoring | pboutill |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-03-20 | Fixing alpha-conversion bug #2723 introduced in r12485-12486. | herbelin |
| 2012-03-14 | Second step of integration of Program: | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-10-11 | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin |
| 2011-06-21 | Cleaning debugging printer relative to new proof engine. In | herbelin |
| 2011-06-13 | Added a flag to restrict conversion in tactic unification on the | herbelin |
| 2011-06-10 | Moved allow_K to a unification flag | herbelin |
| 2011-05-04 | First phase removing obsolete support for eta up to conversion in | herbelin |
| 2011-03-10 | Forgot a use of evars_reset_evd in nf_evars, add an optional argument as | msozeau |
| 2011-03-07 | Reverted commit r13893 about propagation of more informative | herbelin |
| 2011-03-07 | Added propagation of evars unification failure reasons for better | herbelin |
| 2011-02-22 | Try to fix the behavior of clenv_missing used when declaring hints | letouzey |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-15 | Clenv.connect_clenv without its Evd.fold | letouzey |
| 2010-11-07 | Delayed the evar normalization in error messages to the last minute | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-09-17 | In the computation of missing arguments for apply, accept that the | herbelin |
| 2010-08-02 | Fix [clenv_missing] to compute a better approximation of missing | msozeau |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-18 | Quick fix for having clenv debug printer working in trunk. | herbelin |
| 2010-06-13 | Fixed bug #2314 (inversion using not checking the correctness of its arguments | herbelin |
| 2010-06-09 | Fix bug #2317: setoid_rewrite ignored binding lists. Slightly | msozeau |
| 2010-05-10 | Removed an evar_merge in clenv_fchain which not only is incorrect but | 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 |
| 2004-09-03 | deplacement de clenv vers pretyping | barras |
