| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
- marche lorsqu'il n'y rien a reecrire
- marche avec les hypotheses definies (Subst inclut l'Unfold partout)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3450 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3417 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3237 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
constrextern.ml est l'équivalent de termast.ml pour le nouveau
printer; topconstr.ml; contient la définition de "constr_expr";
modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3232 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3218 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Simplification de strength qui est maintenant un simple drapeau Local/Global.
- Export des catégories de déclarations (Lemma/Theorem/Definition/.../
Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml).
- Export des variables de section initialement associées à une déclaration
(nouveau fichier library/dischargedhypsmap.ml).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
précédent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3171 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
variables introduites par NewDestruct et NewInduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3169 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
les erreurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3141 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3139 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
letins, ce qui conduisait a des comportement peu intuitifs. On priviligiera l'utilisation de la tactique Subst.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3103 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3060 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3053 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3045 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3041 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3007 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2993 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- subst_term_gen ne depliait pas les constantes locales de maniere uniforme
- la tactique Simpl ne simplifiait pas les constantes definies dans le
contexte de but
- la conversion d'un constr vers identificateur ne prenait pas en compte
les inductifs et constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2971 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2965 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2963 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
frais de Intro
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2905 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2894 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2882 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
de la forme (E->F)->G.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2868 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2853 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2837 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2779 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2765 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
effacement ne peut être renommée pareille
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2763 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Simplify_eq et Injection
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2757 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
et Injection
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2754 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
rparation de la protection contre les clauses indiscernables de TACTIC EXTEND et VERNAC COMMAND EXTEND; rparation des grammaires de Extraction, EAuto, TextMode, KillProof et Derive Dependent Inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2753 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2743 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2737 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2735 85f007b7-540e-0410-9357-904b9bb8a0f7
|