aboutsummaryrefslogtreecommitdiff
path: root/checker/reduction.ml
AgeCommit message (Expand)Author
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-18Fixing the checker.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-10-02Univs: fix checker generating undeclared universes.Matthieu Sozeau
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-07Checker: Fix bug #4282Matthieu Sozeau
2015-03-23coqchk: more prints when -debugEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2015-01-06improve efficiency of the reduction interpreter of the checkerBruno Barras
2014-09-06Remove debug printing codeMatthieu Sozeau
2014-09-06Cleanup code for looking up projection bodies.Matthieu Sozeau
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly,Matthieu Sozeau
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-05Rename eta_expand_ind_stacks, fix the one from the checker and adaptMatthieu Sozeau
2014-07-22Porting guard fix to checker.Maxime Dénès
2014-06-07Removing 'open Univ' from checker.Pierre-Marie Pédrot
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-05-08Adapt the checker to polymorphic universes and projections (untested).Matthieu Sozeau
2014-03-18Fixing checker with respect to new kernel name structure and hashmaps.Pierre-Marie Pédrot
2013-10-14Getting rid of the use of deprecated elements (from the OCaml standard library).xclerc
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-10-06still some more dead code removalletouzey
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-08-08Updating headers.herbelin
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
2012-03-02Noise for nothingpboutill
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-03-04checker: cleanupglondu
2011-03-04checker: add eta-expansionglondu
2010-09-24Checker: remove some dead codeletouzey
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
2010-07-30adpated the checker to handle coomutative cuts and lazynessbarras
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29After the approval of Bruno, here the patch for the checker.soubiran
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-22Transfers to checker ("let"s in inductive arities + Coq root read-only).herbelin
2008-09-02[checker] basic conversion oracle: expand local vars firstbarras
2008-05-20also fixed conversion of the checkerbarras
2008-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
2008-04-21added the .vo checker (with independent Makefile)barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 08:19:06 +0000