aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* Exit with code 129 when an anomaly occurs.Gravatar Xavier Clerc2014-11-14
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Remove debug printing codeGravatar Matthieu Sozeau2014-09-06
* Cleanup code for looking up projection bodies.Gravatar Matthieu Sozeau2014-09-06
* Fix checker to handle projections with eta and universe polymorphism correctly,Gravatar Matthieu Sozeau2014-09-06
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Fix checking of constants in checker. Prelude can now be checked.Gravatar Matthieu Sozeau2014-09-06
* Remove unused substitution functions in checker.Gravatar Matthieu Sozeau2014-09-05
* Fix checker treatment of inductives using subst_instances instead of subst_un...Gravatar Matthieu Sozeau2014-09-05
* Fix checker/values.ml with latest changes due to projections and universes.Gravatar Matthieu Sozeau2014-09-05
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Port last changes of the guard condition to checker.Gravatar Maxime Dénès2014-08-06
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Porting guard fix to checker.Gravatar Maxime Dénès2014-07-22
* Cleanup substitution inside universe instances, only done through subst_fn now,Gravatar Matthieu Sozeau2014-07-21
* 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