aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Correction bug invert_names (cf bug #1031)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7490 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Léger nettoyage et uniformisation + généralisation du point d'entrée ↵herbelin
ltac pour qu'il retourne les evar git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7361 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-06Un vieux bug d'affichage des lieurs (cf bug #1005)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7346 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19pas besoin de List.length pour savoir si une liste est videletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7306 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-09backtrack sur le typage des instantiations d\'evarsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7129 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-08evar declarees avec mauvais typebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7125 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07pas de filtrages partielsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7121 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07reparations de quelques petits bugs d\'unification + introduction de la ↵barras
notion de variable de sortes (mais pas encore utilise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7120 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-06essai de typage des instantiations d\'evarsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05eradication de Evarutil.w_Definebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7113 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05assouplissement de real_clean: ne tient pas compte des occcurences flexibles ↵barras
des variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7112 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-28unification: evar_define checks the free variables are bound in the evar contextbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7088 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-25Added subtac contrib.coq
Added some debug printer in termops. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24Added clenv_environments_evars that behaves as clen_environments butsacerdot
generating evars in place of metas. Notice that thanks to this changement unification can be more effective (expecially after reduction) since evars have non-empty contexts whereas metas have not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7069 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24WARNING: unification changed (to fix a bug).sacerdot
1. When matching ?i[sigma] against t' in some cases ?i was instantiated with t' ignoring the explicit substitution sigma (i.e. always doing mimick); however, when t' occurs in sigma ?i can be instatiated with a Var/Rel (i.e. doing projection). The new behaviour is not equivalent to the old one (even up to bugs) since the new behaviour may accept not well typed instantiations and fail only later whereas the old (but buggy) behaviour failed immediately. 2. Second bug fixed: it was the case that instantiating and evar doing projection did not check whether the body of the evar contained metavariables (that breaks a Coq invariant). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7067 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵herbelin
reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7048 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Documentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7047 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
convertibility is now tried in setoid_rewrite. As a consequence it is now possible to declare relations over the function space (fun A B: Type => A -> B). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7039 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-29Fix bug in prepare_predicate_from_tycon; improved error message when no ↵herbelin
clauses and no empty inductive type found; (expected) improvement in the shifting test (match_current) on non inductive type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6969 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-15Backtrack sur la substitution combinée avec l'instanciation en réponse à ↵herbelin
l'inefficacité montrée dans le bug #932: suppression plutôt des Anonymous dans le contexte des evars (cf Evarutil) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6836 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-12Backtrack version 1.82 awaiting for better understanding of the consequences ↵herbelin
of removing Anonymous from evars contexts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6828 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-11Méthode plus raisonnable pour supprimer l'inefficacité des evars ↵herbelin
dépendantes de Anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6825 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-10A défaut de substitution paresseuse ou explicite, ajout d'une substitution ↵herbelin
optimisée pour le prétypage qui normalise les evars à la volée (cf bug #932) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6820 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-10A défaut de substitution paresseuse ou explicite, ajout d'une substitution ↵herbelin
optimisée pour le prétypage que normalise les evars (cf bug #932) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6819 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-09bug #931 (continued): no recursion on the evars instantiationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6816 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-08Fix bug #931: leave dependent evars as such for refineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-08Ajout foldherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6811 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-01Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6787 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Standardisation of function names about global references (especially, ↵herbelin
renaming of constr_of_reference into constr_of_global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse ↵herbelin
in recordops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6741 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Ajout it_mkNamedProd_wo_LetInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6740 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Ajout splay_lambdaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6739 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Uniformisation de destApplication en destAppherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6713 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Ajout Print Canonical Structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-02Correction de la précédence des contexts de variables rel, ltac et varherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6660 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body) instead of looking it up in the environment. A version of the same functions with the old type is put in Inductiveops (outside the kernel). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-03HUGE COMMITsacerdot
1. when applying a functor F(X) := B to a module M, the obtained module is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the body of t in M}. In principle it is now easy to fine tune the behaviour to choose whether b or M.t must be used. This change implies modifications both inside and outside the kernel. 2. for each object in the library it is now necessary to define the behaviour w.r.t. the substitution {X.t := b}. Notice that in many many cases the pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken (in the sense that it used to break several invariants). This commit fixes the behaviours for most of the objects, excluded a) coercions: a future commit should allow any term to be declared as a coercion; moreover the invariant that just a coercion path exists between two classes will be broken by the instantiation. b) global references when used as arguments of a few tactics/commands In all the other cases the behaviour implemented is the one that looks to me as the one expected by the user (if possible): [ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ] a) argument scopes: not expanded b) SYNTAXCONSTANT: expanded c) implicit arguments: not expanded d) coercions: expansion to be done (for now not expanded) e) concrete syntax tree for patterns: expanded f) concrete syntax tree for raw terms: expanded g) evaluable references (used by unfold, delta expansion, etc.): not expanded h) auto's hints: expanded when possible (i.e. when the expansion of the head of the pattern is rigid) i) realizers (for program extraction): nothing is done since the actual code does not look for the realizer of definitions with a body; however this solution is fragile. l) syntax and notation: expanded m) structures and canonical structures: an invariant says that no parameter can happear in them ==> the substitution always yelds the original term n) stuff related to V7 syntax: since this part of the code is doomed to disappear, I have made no effort to fix a reasonable semantics; not expanded is the default one applied o) RefArgTypes: to be understood. For now a warning is issued whether expanded != not expanded, and the not expanded solution is chosen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant ↵herbelin
dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-29ExtraRedExpr maintenant sans argument: pas très souple mais au moins ↵herbelin
convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-29Bug control_only_guardherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6524 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Correction du bug de build_initial_predicate a révèlé un autre bug dans ↵herbelin
expand_arg git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6457 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Achèvement correction bug do_restrict_hys: ne pas inverser les argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6454 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6437 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Bugs dans la déclaration du type du terme filtré si non définiherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6433 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 08:15:34 +0000