aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-03-05Canary testing absence of generic equality for KerNamesPierre-Marie Pédrot
2014-03-05Lazily computed hash in KerName.t.Pierre-Marie Pédrot
2014-03-05Adding a canary library. This canary is imperfect. It allows serializationPierre-Marie Pédrot
2014-03-05Fixing compilation on OCaml 4.01.Pierre-Marie Pédrot
2014-03-05Fixing previous commit. Forgot to include some code.Pierre-Marie Pédrot
2014-03-05Added a new module HMap. It works (almost) like Map, except that it expectsPierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-05Correct handling of hashconsing of constraint sets. The previous implementationPierre-Marie Pédrot
2014-03-05Adding a CSet module in Coq lib.Pierre-Marie Pédrot
2014-03-04Fixing pervasives equalities in Vconv.Pierre-Marie Pédrot
2014-03-04Move error and job display to the lower right pane.Guillaume Melquiond
2014-03-04STM: fix Show ScriptEnrico Tassi
2014-03-04STM: when finish a task hcons universe constraintsEnrico Tassi
2014-03-03Fixing some generic equalities in Micromega.Pierre-Marie Pédrot
2014-03-03Fixing Pervasives.equality in extraction.Pierre-Marie Pédrot
2014-03-03Fixing pervasive equalities. In particular, I removed the code that deletedPierre-Marie Pédrot
2014-03-03Removing generic hashes in kernel.Pierre-Marie Pédrot
2014-03-03Getting rid of generic hashes in cc plugin.Pierre-Marie Pédrot
2014-03-03Kernel names are implemented using records.Pierre-Marie Pédrot
2014-03-03Goptions do not rely anymore on generic equality.Pierre-Marie Pédrot
2014-03-03Term dnets do no need to contain the afferent constr pattern in their nodes.Pierre-Marie Pédrot
2014-03-03Removing Termdn, and putting the relevant code in Btermdn. The current TermdnPierre-Marie Pédrot
2014-03-03Extruding code not depending of the functor argument in Termdn.Pierre-Marie Pédrot
2014-03-03Replacing arguments of Trie by a cancellable monoid.Pierre-Marie Pédrot
2014-03-03Fixing generic hashes and replacing them with proper ones.Pierre-Marie Pédrot
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
2014-03-02Set officially the minimal OCaml requirement to 3.12.1Pierre Letouzey
2014-03-02Makefile: the initial build of grammar.cma is now directory-drivenPierre Letouzey
2014-03-02Migrate back g_obligations in toplevelPierre Letouzey
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-03-02Removing generic equality in Syntax plugin.Pierre-Marie Pédrot
2014-03-02Adding an equality function over glob_constrPierre-Marie Pédrot
2014-03-02Fixing generic Hashtbl.hash in Constr.Pierre-Marie Pédrot
2014-03-02Fix syntax highlighting of "Implicit Arguments" for gtksourceview.Guillaume Melquiond
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2014-03-01Better behaviour for sets of reserved names.Pierre-Marie Pédrot
2014-03-01Never suppress the typing constraint of bound variables whose name wasPierre-Marie Pédrot
2014-03-01Fixing bad comparison in Detyping.Pierre-Marie Pédrot
2014-03-01Useless check when loading notations through import.Pierre-Marie Pédrot
2014-03-01Hunting pervasive equality in native compiler. It seems they were used forPierre-Marie Pédrot
2014-03-01Removing a fishy use of pervasive equality in Ltac backtrace printing.Pierre-Marie Pédrot
2014-02-28Removing Pervasives.compare in Termdn.Pierre-Marie Pédrot
2014-02-28Removing a Pervasives.compare in Term_dnet.Pierre-Marie Pédrot
2014-02-28Pos.compare_cont takes the comparison as first argumentPierre Boutillier
2014-02-28Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini...Pierre Boutillier
2014-02-28test-suite: opaque term -> opaque proofPierre Boutillier
2014-02-28test-suite: New names for vars but the expected invariant is preservedPierre Boutillier
2014-02-28Fix output test-suite 'simpl tactic' -> 'reduction tactics'Pierre Boutillier
2014-02-28Dead code elimionation in reductionopsPierre Boutillier
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:14:21 +0000