| Commit message (Expand) | Author | Age |
* | Allowing different types of, not to be mixed, generic Stores through | ppedrot | 2013-03-12 |
* | Locating errors from consider_remaining_unif_problems if possible | herbelin | 2013-02-17 |
* | Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env | herbelin | 2013-01-29 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Monomorphization (pretyping) | ppedrot | 2012-11-22 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | remove many excessive open Util & Errors in mli's | letouzey | 2012-05-29 |
* | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey | 2012-05-29 |
* | Adds a comment: precondition on Evd.add | aspiwack | 2012-04-18 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Introducing a notion of evar candidates to be used when an evar is | herbelin | 2011-12-16 |
* | Continuing r14585 (ill-typed restriction bug). | herbelin | 2011-10-25 |
* | Cleaning debugging printer relative to new proof engine. In | herbelin | 2011-06-21 |
* | Added a new flag for freezing evars in tactic unification. Used this | herbelin | 2011-06-12 |
* | A better procedure for checking presence of undefined evars. | aspiwack | 2011-05-13 |
* | First phase removing obsolete support for eta up to conversion in | herbelin | 2011-05-04 |
* | 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-11 |
* | Forgot a use of evars_reset_evd in nf_evars, add an optional argument as | msozeau | 2011-03-10 |
* | - Use transparency information all the way through unification and | msozeau | 2011-02-17 |
* | Misc improvements about evar_map | letouzey | 2010-12-15 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Added Chung-Kil Hur's smart "pattern" tactic (h_resolve). | herbelin | 2010-06-22 |
* | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
* | Improved the efficiency of evars traverals thanks to a split of | herbelin | 2010-05-13 |
* | Deux commentaires retirés de ocamldoc. | aspiwack | 2010-05-07 |
* | Various minor improvements of comments in mli for ocamldoc | letouzey | 2010-04-29 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill | 2010-04-29 |
* | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
* | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin | 2009-12-24 |
* | Attached evar source to the evar_info and add location to tclWITHHOLES errors | herbelin | 2009-12-22 |
* | In "progress", extending the set of evars w/o solving an existing one is | herbelin | 2009-12-21 |
* | Promote evar_defs to evar_map (in Evd) | glondu | 2009-11-11 |
* | - Fixed a bug in checking that implicit arguments are all correctly | herbelin | 2009-09-18 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Backtrack on experimental unification with sort variables: it requires | msozeau | 2009-06-02 |
* | Change unification with sort constraints to not use the kernel | msozeau | 2009-06-01 |
* | Populate the sort constraints set correctly during unification. Add a | msozeau | 2009-05-27 |
* | A try at using sort variables during unification. Instead of refreshing | msozeau | 2009-05-23 |
* | - Fixing bug #2084 (unification not checking sort constraints), hoping | herbelin | 2009-04-08 |
* | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau | 2009-03-28 |
* | Backtrack sur la mémoïsation de nf_evar. | aspiwack | 2009-03-04 |
* | =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=... | aspiwack | 2009-02-27 |
* | On passe les last_mods (un des champs de Evd.evar_defs) de list | aspiwack | 2009-02-20 |
* | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack | 2009-02-19 |
* | Really compare evar maps in progress, due to merging in apply and other | msozeau | 2009-01-23 |
* | DISCLAIMER | puech | 2009-01-17 |