| Age | Commit message (Expand) | Author |
|---|
| 2013-04-15 | More functional implementation of locality_flag and program_mode | gareuselesinge |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-25 | Monomorphization (tactics) | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-01 | More cleaning | ppedrot |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-05-29 | Pattern as a mli-only file, operations in Patternops | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey |
| 2012-04-12 | Remove print call that do not use the pp mechanism | pboutill |
| 2012-03-30 | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-09-23 | auto with nocore : disable the use of the core database (wish #2188) | letouzey |
| 2011-06-10 | Moved allow_K to a unification flag | herbelin |
| 2011-03-11 | - Better error messages taking unif. constraints into account. | msozeau |
| 2011-03-04 | - Allow to set a particular transparent_state for the local hint | msozeau |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-10-31 | An experimental support for open constrs in hints and in "using" | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-27 | Minor fixes: | msozeau |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-12 | Fixing spelling: pr_coma -> pr_comma | herbelin |
| 2010-06-03 | Avoid computing tactic printing tree (std_ppcmds) when printing not needed in | 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-17 | Use nice "unfold" instead of ugly "change" to display calls to unfold hints | herbelin |
| 2010-03-05 | Fix [autounfold] to accept general [in] clauses. | msozeau |
| 2009-11-06 | Misc fixes. | msozeau |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-07-14 | Simplify eauto and fix it for compatibility, allowing full delta during | msozeau |
| 2009-07-09 | Use the proper unification flags in e_exact. This makes exact fail a bit | msozeau |
| 2009-04-08 | Some dead code removal + cleanups | letouzey |
| 2008-12-28 | - Another bug in get_sort_family_of (sort-polymorphism of constants and | herbelin |
| 2008-12-26 | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin |
| 2008-12-16 | Finish fix for the treatment of [inverse] in [setoid_rewrite], making a | msozeau |
| 2008-12-14 | Fix looping class resolution bug discovered by B. Aydemir and use the | msozeau |
| 2008-09-07 | Add the ability to declare [Hint Extern]'s with no pattern. | msozeau |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-06-27 | Enhanced discrimination nets implementation, which can now work with | msozeau |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-05-01 | Move exception-handling code for catching tactics failure | msozeau |
| 2008-04-29 | Fix eauto still using delta when it shouldn't (should make CoRN compile | msozeau |
