aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Collapse)Author
2002-12-23Tentative d'interdire les K-abstractions si allow_K est faux et leherbelin
motif n'a pas de métas (dans unify_to_subterm_list) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3479 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-22Cas motif universelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3476 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3472 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-20Prise en compte des coercions dans les 'with' bindingsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3468 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19simplification de solve_subgoal: n'utilise plus frontierbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3458 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19suite du commit precedentbarras
- amelioration des messages d'erreurs de la condition de garde - reorganisation de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3457 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-13Compensation de suppression betaiota de type_of (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3433 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-12Compensation de suppression betaiota de type_of (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3427 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-12Ajout du vernac Proof withgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-11Compensation de suppression betaiota de type_ofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3421 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Option pour rendre les vérifications du refiner optionnelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Option pour rendre les vérifications du refiner optionnelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3393 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- 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
2002-11-13simplification common_ancestorcourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3229 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- 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
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
variables introduites par NewDestruct et NewInduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3169 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
les erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3141 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3121 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-09retour en arriere concernant la recherche d'occurence modulo expansion des ↵barras
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
2002-10-01Vraie substitutivite de autohintscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13Renoncement à distinguer les types "constr" et "types"; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2964 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-24Ajout d'un point d'entree pour exporter les arbres de preuves en XMLherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2917 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-23MAJ commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2909 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Protection contre l'encapsulage de FailError dans Exc_located (sinon, par ↵herbelin
exemple, 'Try Tauto' ne marche pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2855 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-14Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2786 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-13Bug non vérification non redondance par Cutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2784 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Déplacement de proofs vers tacticsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2732 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Réorganisation des tclTHEN (cf dev/changements.txt)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2721 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichier des expressions de tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2714 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-27Ajout de Eval, Inst et Checkdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2711 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
gauche à droite des hypothèses dans Intuition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2696 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Finalement VTactic est gardé pour y plonger les tactiques ML, leherbelin
VTactic utilisé pour les fermetures de ltac s'appelle maintenant VTacticClos git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2693 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Contournement de la fermeture ML dans VContextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2691 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14- Changement de l'ordre de filtrage dans "Match Context"herbelin
- Protection des "Match Context" contre les exceptions non UserError ni Fail - Remplacement des fermetures ML dans VTactic et VFTactic par des expressions de tactiques pour permettre l'intégration de Tactic Definition dans les états - Changement en conséquence de Tauto git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2685 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14modification de clenv_merge:barras
on ajoute en premier lieu les contraintes concernant le terme puis apres celles concernant le type de chaque instantiation, au lieu d'alterner l'ajout de contraintes de terme et de type. A l'essai. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2682 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17typed unification in the case of Patternbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2654 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12backtrack unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2642 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12q: Commande introuvable.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2640 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12Re-introduction de clenv_constrain_missing_arg utilisé par la contrib Lannionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2634 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-11Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2632 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10backtrack dans l'algo d'unificationbarras
fichier usage incorrect (libdir et bindir ont disparu) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2629 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Simplification des Clear internes dégénérés (sans hypothèses à effacer)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2626 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-04resolution du pb d'efficacite du a Sign.add_named_declbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-03transformation des evar en meta preserve la linearite des metasbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2605 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-03changement de l'undo limitbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2604 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 17:11:18 +0000