aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Adding phantom types to discriminate normalized goals, and adding a way toGravatar Pierre-Marie Pédrot2014-03-19
* Remove the -fno-defer-pop cflagGravatar Jason Gross2014-03-18
* Printing backtraces in coqchk while in debug mode.Gravatar Pierre-Marie Pédrot2014-03-18
* Fixing checker with respect to new kernel name structure and hashmaps.Gravatar Pierre-Marie Pédrot2014-03-18
* STM: make the slave start from the most recent known stateGravatar Enrico Tassi2014-03-18
* STM: make -async-proofs on work from coqc tooGravatar Enrico Tassi2014-03-18
* Evarconv: exact_ise_stack looks to stack head before bodies or branchesGravatar Pierre Boutillier2014-03-17
* Fix test-suite 2255.vGravatar Pierre Boutillier2014-03-17
* consider_remaining_unif_problems respects Conv_oracleGravatar Pierre Boutillier2014-03-16
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
* nanoPG: better copy/pasteGravatar Enrico Tassi2014-03-13
* fix compilation with ocaml < 4Gravatar Enrico Tassi2014-03-13
* STM: perspective (tell the scheduler what the user sees)Gravatar Enrico Tassi2014-03-13
* Stateid: export a Set moduleGravatar Enrico Tassi2014-03-13
* STM: move out a couple of submodulesGravatar Enrico Tassi2014-03-13
* fake_ide: fix compilationGravatar Enrico Tassi2014-03-12
* Stm: smarter delegation policyGravatar Enrico Tassi2014-03-12
* CoqIDE: Errors page gets red if not emptyGravatar Enrico Tassi2014-03-12
* CoqIDE: detachable message/error/jobs panesGravatar Enrico Tassi2014-03-12
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Fix (3243): univ constraints of module subtyping were not propagatedGravatar Enrico Tassi2014-03-11
* Useless Array.to_list in Typeops.Gravatar Pierre-Marie Pédrot2014-03-10
* Evarconv unification respects Conv_oracleGravatar Pierre Boutillier2014-03-10
* MaybeFlexible semantic changesGravatar Pierre Boutillier2014-03-10
* Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Gravatar Guillaume Melquiond2014-03-10
* Using HMaps in global references.Gravatar Pierre-Marie Pédrot2014-03-08
* Also use HMaps in KNmap.Gravatar Pierre-Marie Pédrot2014-03-08
* Potentially unused computation in Goal.Gravatar Pierre-Marie Pédrot2014-03-07
* Useless tactic bindings in Tacticals.Gravatar Pierre-Marie Pédrot2014-03-07
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
* Tentative fix for a very strange pervasive equality in Auto.Gravatar Pierre-Marie Pédrot2014-03-07
* Compiling coqc in "tools" target.Gravatar Pierre-Marie Pédrot2014-03-07
* Fix lookup of native files when option -R is missing.Gravatar Guillaume Melquiond2014-03-07
* Fixing generic equality in Auto.Gravatar Pierre-Marie Pédrot2014-03-07
* Inductive maps in Environ now use HMap.Gravatar Pierre-Marie Pédrot2014-03-06
* make install-coqlight installs DLLCOQRUN and LIBCOQRUNGravatar Pierre Boutillier2014-03-06
* Lets coqtop use a slashGravatar Virgile Prevosto2014-03-06
* Uses slashes for install and config directoriesGravatar Virgile Prevosto2014-03-06
* remove trailing '\r' from file names returned by coqtopGravatar Virgile Prevosto2014-03-06
* Fix typo in comment.Gravatar Maxime Dénès2014-03-05
* Fixing interpretation of tactics in terms. It was forgetting part of theGravatar Pierre-Marie Pédrot2014-03-06
* Using HMaps in Safe_env.environments, hopefully improving performances.Gravatar Pierre-Marie Pédrot2014-03-05
* Canary testing absence of generic equality for KerNamesGravatar Pierre-Marie Pédrot2014-03-05
* Lazily computed hash in KerName.t.Gravatar Pierre-Marie Pédrot2014-03-05
* Adding a canary library. This canary is imperfect. It allows serializationGravatar Pierre-Marie Pédrot2014-03-05
* Fixing compilation on OCaml 4.01.Gravatar Pierre-Marie Pédrot2014-03-05
* Fixing previous commit. Forgot to include some code.Gravatar Pierre-Marie Pédrot2014-03-05
* Added a new module HMap. It works (almost) like Map, except that it expectsGravatar Pierre-Marie Pédrot2014-03-05
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 03:13:16 +0000