aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fixing some generic equalities in Micromega.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing Pervasives.equality in extraction.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing pervasive equalities. In particular, I removed the code that deletedGravatar Pierre-Marie Pédrot2014-03-03
* Removing generic hashes in kernel.Gravatar Pierre-Marie Pédrot2014-03-03
* Getting rid of generic hashes in cc plugin.Gravatar Pierre-Marie Pédrot2014-03-03
* Kernel names are implemented using records.Gravatar Pierre-Marie Pédrot2014-03-03
* Goptions do not rely anymore on generic equality.Gravatar Pierre-Marie Pédrot2014-03-03
* Term dnets do no need to contain the afferent constr pattern in their nodes.Gravatar Pierre-Marie Pédrot2014-03-03
* Removing Termdn, and putting the relevant code in Btermdn. The current TermdnGravatar Pierre-Marie Pédrot2014-03-03
* Extruding code not depending of the functor argument in Termdn.Gravatar Pierre-Marie Pédrot2014-03-03
* Replacing arguments of Trie by a cancellable monoid.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Set officially the minimal OCaml requirement to 3.12.1Gravatar Pierre Letouzey2014-03-02
* Makefile: the initial build of grammar.cma is now directory-drivenGravatar Pierre Letouzey2014-03-02
* Migrate back g_obligations in toplevelGravatar Pierre Letouzey2014-03-02
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Removing generic equality in Syntax plugin.Gravatar Pierre-Marie Pédrot2014-03-02
* Adding an equality function over glob_constrGravatar Pierre-Marie Pédrot2014-03-02
* Fixing generic Hashtbl.hash in Constr.Gravatar Pierre-Marie Pédrot2014-03-02
* Fix syntax highlighting of "Implicit Arguments" for gtksourceview.Gravatar Guillaume Melquiond2014-03-02
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Better behaviour for sets of reserved names.Gravatar Pierre-Marie Pédrot2014-03-01
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
* Fixing bad comparison in Detyping.Gravatar Pierre-Marie Pédrot2014-03-01
* Useless check when loading notations through import.Gravatar Pierre-Marie Pédrot2014-03-01
* Hunting pervasive equality in native compiler. It seems they were used forGravatar Pierre-Marie Pédrot2014-03-01
* Removing a fishy use of pervasive equality in Ltac backtrace printing.Gravatar Pierre-Marie Pédrot2014-03-01
* Removing Pervasives.compare in Termdn.Gravatar Pierre-Marie Pédrot2014-02-28
* Removing a Pervasives.compare in Term_dnet.Gravatar Pierre-Marie Pédrot2014-02-28
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
* Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini...Gravatar Pierre Boutillier2014-02-28
* test-suite: opaque term -> opaque proofGravatar Pierre Boutillier2014-02-28
* test-suite: New names for vars but the expected invariant is preservedGravatar Pierre Boutillier2014-02-28
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
* Dead code elimionation in reductionopsGravatar Pierre Boutillier2014-02-28
* .*.aux erased by make distcleanGravatar Pierre Boutillier2014-02-28
* Fix compilation of coq and plugins using coq_makefile under cygwinGravatar Enrico Tassi2014-02-28
* Fixing a Pervasive.compare.Gravatar Pierre-Marie Pédrot2014-02-28
* Makefile: re-introduce 2 phases to avoid make strange -include'sGravatar Pierre Letouzey2014-02-27
* amending last commitGravatar Enrico Tassi2014-02-27
* better warningGravatar Enrico Tassi2014-02-27
* Tacinterp: more refactoring.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
* Get rid of the enterl/glist API for Proofview.Goal.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: yet another superfluous enterl.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: spurious enterl.Gravatar Arnaud Spiwack2014-02-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 03:47:47 +0000