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