aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-03-12Stm: smarter delegation policyEnrico Tassi
2014-03-12CoqIDE: Errors page gets red if not emptyEnrico Tassi
2014-03-12CoqIDE: detachable message/error/jobs panesEnrico Tassi
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-11Fix (3243): univ constraints of module subtyping were not propagatedEnrico Tassi
2014-03-10Useless Array.to_list in Typeops.Pierre-Marie Pédrot
2014-03-10Evarconv unification respects Conv_oraclePierre Boutillier
2014-03-10MaybeFlexible semantic changesPierre Boutillier
2014-03-10Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Guillaume Melquiond
2014-03-08Using HMaps in global references.Pierre-Marie Pédrot
2014-03-08Also use HMaps in KNmap.Pierre-Marie Pédrot
2014-03-07Potentially unused computation in Goal.Pierre-Marie Pédrot
2014-03-07Useless tactic bindings in Tacticals.Pierre-Marie Pédrot
2014-03-07Using Hashmaps by default in constant and inductive maps. This changes fold andPierre-Marie Pédrot
2014-03-07Tentative fix for a very strange pervasive equality in Auto.Pierre-Marie Pédrot
2014-03-07Compiling coqc in "tools" target.Pierre-Marie Pédrot
2014-03-07Fix lookup of native files when option -R is missing.Guillaume Melquiond
2014-03-07Fixing generic equality in Auto.Pierre-Marie Pédrot
2014-03-06Inductive maps in Environ now use HMap.Pierre-Marie Pédrot
2014-03-06make install-coqlight installs DLLCOQRUN and LIBCOQRUNPierre Boutillier
2014-03-06Lets coqtop use a slashVirgile Prevosto
2014-03-06Uses slashes for install and config directoriesVirgile Prevosto
2014-03-06remove trailing '\r' from file names returned by coqtopVirgile Prevosto
2014-03-05Fix typo in comment.Maxime Dénès
2014-03-06Fixing interpretation of tactics in terms. It was forgetting part of thePierre-Marie Pédrot
2014-03-05Using HMaps in Safe_env.environments, hopefully improving performances.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 22:42:09 +0000