aboutsummaryrefslogtreecommitdiff
path: root/checker/reduction.ml
AgeCommit message (Collapse)Author
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
in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk?
2015-07-07Checker: Fix bug #4282Matthieu Sozeau
Adapt to new [projection] abstract type comprising a constant and a boolean.
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
Conflicts: checker/closure.ml checker/closure.mli checker/reduction.ml
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
simplifying conversion code.
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
it to the new representation of projections and the new mind_finite type.
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
Some wrong generic equalities and hashes were removed too.
2013-10-14Getting rid of the use of deprecated elements (from the OCaml standard library).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Uniformization of the "anomaly" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06still some more dead code removalletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
Same for check_leq instead of check_geq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Esubst: make types of substitutions & lifts privatepuech
Allows to be sure that we apply the smart constructors. Propagate the change to Closure, Reduction, Term, Cbv and Newring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-04checker: cleanupglondu
Backport of changes introduced in r13443. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13867 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-04checker: add eta-expansionglondu
Backport of changes introduced in r13443 and r13494. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13866 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Checker: remove some dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
This commit fixes a bug that made the system inconsistent with proof irrelevance (the main idea being that Set = Prop by reflexivity). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13450 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30adpated the checker to handle coomutative cuts and lazynessbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13365 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29After the approval of Bruno, here the patch for the checker.soubiran
In checker: - delta_resolver inferred by the module system is checked through regular delta reduction steps - the old mind_equiv field of mutual_inductive is simulated through a special table in environ - small optimization, if the signature and the implementation of a module are physically equal (always happen for the toplevel module of a vo) then the checker checks only the signature. In kernel - in names i have added two special equality functions over constant and inductive names for the checker, so that the checker does not take in account the cannonical name inferred by the module system. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12977 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-22Transfers to checker ("let"s in inductive arities + Coq root read-only).herbelin
- Support for let's in the signature of the arity of an inductive type was in the kernel part of commit 12273, - Support for binding Coq root read-only in -R option was in commit 12220. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12288 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-02[checker] basic conversion oracle: expand local vars firstbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11345 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20also fixed conversion of the checkerbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10953 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
univers, suite à discussion avec Bruno : on franchit le cap et on ajoute le sous-typage Prop <= Set. On n'a donc plus besoin d'utiliser l'image de Prop dans la hiérarchie en dehors de la zone de calcul de la sorte la plus basse d'un inductif polymorphe (au passage, nous avons décidé de renommer Type -1 en Type 0-, pour bien indiquer qu'il se trouve au même niveau que Type 0). Coq se retrouve donc avec la hiérarchie Prop <= Set <= Type i et avec une copie de Prop (Type 0-) et une copie de Set (Type 0) dans la hiérarchie Type. En théorie, on pourrait donc supprimer "Prop Null" et "Prop Pos" de l'implémentation et ne travailler qu'avec "Type". L'ajout de Prop <= Set vaut à la fois dans le cas Set prédicatif et dans le cas Set imprédicatif (Prop et Set étant en bas de la hiérarchie, il n'y a pas d'incohérence connue). Dans le modéle ensembliste, Prop et Type 0- sont interprétés par exemple comme {{},{o}}, où "o" est un objet particulier interprétant les preuves, et il n'y a pas de Set imprédicatif. Dans un modèle de réalisabilité, Set imprédicatif est interprétable et Prop peut au choix s'interpréter comme Set ou comme booléen (cf la thèse de Miquel). Le sous-typage du côté ensembliste s'obtient en mettant au moins l'ensemble {{},{o}} dans l'interprétation de Set (ce qu'on fait de la même manière que Prop <= Type 1, avec conversion typée), et du côté réalisabilité en mettant l'ensemble {Typ(vide),Typ(unit)} dans l'interprétation de Set ("Typ" étant la coercion faisant d'un ensemble un terme), ce qui est fait dans la section 6.2.4 de la thèse d'Alexandre Miquel (modèle du CC implicite sans types inductifs). Il reste un problème pratique. Lorsqu'on donne Inductive unit:Type := tt:unit. Coq dit que unit est dans Prop. C'est correct parce qu'il n'y a pas de contraintes d'univers mais un peu déroutant même si la coercion "unit : Set" reste valide. Une suggestion est de ne rendre polymorphe que les inductifs dont on ne donne pas la sorte explicitement, comme dans Inductive unit := tt:unit. mais alors, comment indiquer l'absence de sorte explicite si le type a des paramètres réels (comme "vect") ?? PS: modification de sort_cmp dans checker/inductive.ml faite. --This line, and those below, will be ignored-- M kernel/univ.ml M kernel/univ.mli M kernel/inductive.ml M kernel/reduction.ml M kernel/indtypes.ml M checker/inductive.ml M checker/reduction.ml M pretyping/reductionops.ml M pretyping/termops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10920 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-21added the .vo checker (with independent Makefile)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10826 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 16:22:27 +0000