aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-03-19Using non-normalized goals in tactic interpretation.Pierre-Marie Pédrot
2014-03-19Adding phantom types to discriminate normalized goals, and adding a way toPierre-Marie Pédrot
2014-03-18Remove the -fno-defer-pop cflagJason Gross
2014-03-18Printing backtraces in coqchk while in debug mode.Pierre-Marie Pédrot
2014-03-18Fixing checker with respect to new kernel name structure and hashmaps.Pierre-Marie Pédrot
2014-03-18STM: make the slave start from the most recent known stateEnrico Tassi
2014-03-18STM: make -async-proofs on work from coqc tooEnrico Tassi
2014-03-17Evarconv: exact_ise_stack looks to stack head before bodies or branchesPierre Boutillier
2014-03-17Fix test-suite 2255.vPierre Boutillier
2014-03-16consider_remaining_unif_problems respects Conv_oraclePierre Boutillier
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
2014-03-13nanoPG: better copy/pasteEnrico Tassi
2014-03-13fix compilation with ocaml < 4Enrico Tassi
2014-03-13STM: perspective (tell the scheduler what the user sees)Enrico Tassi
2014-03-13Stateid: export a Set moduleEnrico Tassi
2014-03-13STM: move out a couple of submodulesEnrico Tassi
2014-03-12fake_ide: fix compilationEnrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 22:59:05 +0000