aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06- Fix comparison of universes.Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-29Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunatelyHugo Herbelin
2014-04-28Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toHugo Herbelin
2014-04-10Fix guard condition for nested cofixpoints in checker.Maxime Dénès
2014-04-08printer for coqchkEnrico Tassi
2014-04-04Fixing coqchk. It was my fault, I misused canonical and user equalitiesPierre-Marie Pédrot
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-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-05Adding a canary library. This canary is imperfect. It allows serializationPierre-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 many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-05Adding a CSet module in Coq lib.Pierre-Marie Pédrot
2014-02-26checker and votour ported to new vo format (after -vi2vo)Enrico Tassi
2014-02-26votour: better error messagesEnrico Tassi
2014-02-26checker: less useless error messagesEnrico Tassi
2014-02-26fix checker w.r.t. mutual_inductive_body and constant_bodyEnrico Tassi
2014-02-26fix checker w.r.t. Dyn.t validationEnrico Tassi
2014-01-19Fixing checker compilation, which was broken by the following commit:Pierre-Marie Pédrot
2014-01-18Relaxing the sort elimination check to allow for let-bindings in arities.Maxime Dénès
2014-01-15Christmas is over...Maxime Dénès
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24inductive.ml : get rid of some obvious (Lazy.force (lazy t))letouzey
2013-10-24Rtree : cleanup of the comparing codeletouzey
2013-10-24Get rid of polymorphic equality in "checker/subtyping.ml".xclerc
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-10-18Ephemeron: marshaling friendly keysgareuselesinge
2013-10-14Getting rid of the use of deprecated elements (from the OCaml standard library).xclerc
2013-09-14Slightly more compact representation of 'a substituted type,ppedrot
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-23Adding dynamic value printing to votour through a registering mechanism.ppedrot
2013-08-22Misc changes around coqtop.ml :letouzey
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
2013-08-20Fixing votourppedrot
2013-08-20Fix compilation of coqcheckgareuselesinge
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Repair coqcheck : constant_body constraints are also futureletouzey
2013-08-09checker validation fixed w.r.t. Futuresgareuselesinge
2013-08-09checker validation made a bit more verbosegareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-07-17Declaremods: major refactoring, stop duplicating libobjects in modulesletouzey
2013-05-12Added a generic notion of hook. Hooks are functions to be setppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:29:24 +0000