| Commit message (Expand) | Author | Age |
* | 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-06-04 |
* | code simplifications concerning Summary | letouzey | 2013-04-22 |
* | Restrict (try...with...) to avoid catching critical exn (part 10) | letouzey | 2013-03-13 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Moved Stringset and Stringmap to String namespace. | ppedrot | 2012-12-14 |
* | Monomorphization (tactics) | ppedrot | 2012-11-25 |
* | Removed many calls to OCaml generic equality. This was done by | ppedrot | 2012-10-29 |
* | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey | 2012-10-16 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | 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-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | Cleaning Pp.ppnl use | ppedrot | 2012-06-01 |
* | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey | 2012-05-29 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Merge subinstances branch by me and Tom Prince. | msozeau | 2011-11-17 |
* | Add type annotations around all calls to Libobject.declare_object | letouzey | 2011-11-02 |
* | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin | 2011-10-11 |
* | Relaxed the constraint introduced in r14190 that froze the existing | herbelin | 2011-06-18 |
* | Moved allow_K to a unification flag | herbelin | 2011-06-10 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
* | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
* | Added a function in typing.ml to solve evars of a constr w/o going back down ... | herbelin | 2010-04-05 |
* | Updated compatibility for rewriting equality proofs that are dependent | herbelin | 2009-12-12 |
* | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
* | This big commit addresses two problems: | soubiran | 2009-10-21 |
* | Remove useless Liboject.export_function field | glondu | 2009-09-17 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Death of "survive_module" and "survive_section" (the first one was | herbelin | 2009-08-13 |
* | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin | 2009-08-06 |
* | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau | 2009-06-30 |
* | - Fix handling of clauses in setoid_rewrite to rewrite under binders | msozeau | 2009-04-17 |
* | Rewrite autorewrite to use a dnet indexed by the left-hand sides (or | msozeau | 2009-04-14 |
* | Rewrite of setoid_rewrite to modularize it based on proof-producing | msozeau | 2009-04-13 |
* | Some dead code removal + cleanups | letouzey | 2009-04-08 |
* | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
* | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin | 2008-06-10 |
* | Prise en compte des coercions dans les clauses "with" même si le type | herbelin | 2008-04-23 |
* | Adding 'at' to rewrite, as it is already implemented in setoid_rewrite. | msozeau | 2008-04-12 |
* | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin | 2007-04-28 |
* | Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s... | herbelin | 2006-09-21 |
* | + Changing "in <hyp>" to "in <clause>" (no at, no InValue and no | jforest | 2006-08-22 |
* | Correction bug #1097 (dû à une typo...) | herbelin | 2006-03-02 |
* | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin | 2006-01-11 |
* | Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*... | herbelin | 2005-12-26 |