aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Removing dead code in checker/univ.ml.Gravatar Pierre-Marie Pédrot2014-06-10
* Removing explanations of universe inconsistencies from the checker. TheyGravatar Pierre-Marie Pédrot2014-06-10
* Providing the checker with its own version of the Univ file.Gravatar Pierre-Marie Pédrot2014-06-10
* Removing 'open Univ' from checker.Gravatar Pierre-Marie Pédrot2014-06-07
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* - Fix comparison of universes.Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunatelyGravatar Hugo Herbelin2014-04-29
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* Fix guard condition for nested cofixpoints in checker.Gravatar Maxime Dénès2014-04-10
* printer for coqchkGravatar Enrico Tassi2014-04-08
* Fixing coqchk. It was my fault, I misused canonical and user equalitiesGravatar Pierre-Marie Pédrot2014-04-04
* 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
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Adding a canary library. This canary is imperfect. It allows serializationGravatar 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 many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Adding a CSet module in Coq lib.Gravatar Pierre-Marie Pédrot2014-03-05
* checker and votour ported to new vo format (after -vi2vo)Gravatar Enrico Tassi2014-02-26
* votour: better error messagesGravatar Enrico Tassi2014-02-26
* checker: less useless error messagesGravatar Enrico Tassi2014-02-26
* fix checker w.r.t. mutual_inductive_body and constant_bodyGravatar Enrico Tassi2014-02-26
* fix checker w.r.t. Dyn.t validationGravatar Enrico Tassi2014-02-26
* Fixing checker compilation, which was broken by the following commit:Gravatar Pierre-Marie Pédrot2014-01-19
* Relaxing the sort elimination check to allow for let-bindings in arities.Gravatar Maxime Dénès2014-01-18
* Christmas is over...Gravatar Maxime Dénès2014-01-15
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* inductive.ml : get rid of some obvious (Lazy.force (lazy t))Gravatar letouzey2013-10-24
* Rtree : cleanup of the comparing codeGravatar letouzey2013-10-24
* Get rid of polymorphic equality in "checker/subtyping.ml".Gravatar xclerc2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Ephemeron: marshaling friendly keysGravatar gareuselesinge2013-10-18
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
* Slightly more compact representation of 'a substituted type,Gravatar ppedrot2013-09-14
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Adding dynamic value printing to votour through a registering mechanism.Gravatar ppedrot2013-08-23
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 17:45:57 +0000