aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Prise en compte des variables de grammaires de tactiques et dédollarisation ↵Gravatar herbelin2003-04-08
| | | | | | des metaident git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
| | | | | | | | | pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2003-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack du commit de Christine, qui posait probleme avec FTCGravatar letouzey2003-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Replace aux égalités entre preuvesGravatar herbelin2003-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3833 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un message à FailTac; localisation des appels à des tactiques ↵Gravatar herbelin2003-03-31
| | | | | | définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3824 85f007b7-540e-0410-9357-904b9bb8a0f7
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
| | | | | | | idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed Relative names not,iff in Camlp4 quotation.Gravatar corbinea2003-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing Christine's Intuition1 and adding some invertible hyps.Gravatar corbinea2003-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3780 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changed Tauto so it displays less 'Unfold not iff'Gravatar corbinea2003-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3706 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug introduit dans le backtracking d'occurrenceGravatar delahaye2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chargement dynamique de .cmaGravatar delahaye2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debugger plus informatifGravatar delahaye2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'élimination des existentiels dans LinearIntuition.Gravatar corbinea2003-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3663 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un type "standardisé" pour new_hypGravatar herbelin2003-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3611 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).Gravatar corbinea2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mauvais environnement d'évaluation pour les globauxGravatar herbelin2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug réecriture à la racine pour le sétoide Prop.Gravatar clrenard2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueurGravatar herbelin2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mauvaise interprétatin de IdentArgTypeGravatar herbelin2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3550 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les noms de tactiques inconnus; restriction exceptions ↵Gravatar herbelin2003-01-20
| | | | | | rattrapées dans les Match git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petits bugsGravatar herbelin2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3540 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation d'une exception 'catchable'Gravatar herbelin2003-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3535 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵Gravatar herbelin2003-01-19
| | | | | | la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵Gravatar herbelin2003-01-19
| | | | | | la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3529 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subst sur une hyp qui n'existe pas ne fait pas une anomalieGravatar barras2003-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3515 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction de bug de Subst: ne faisait rien lorsque l'hypotheseGravatar barras2003-01-09
| | | | | | | n'apparaissait que dans le but... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commentaires; optimisationGravatar herbelin2002-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3486 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation du second-ordre avec possibilité de K-rédex dans lemInvGravatar herbelin2002-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3482 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2002-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-essai de forcer le terme réécrit à apparaître dans le butGravatar herbelin2002-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur la tentative d'interdire les K-abstractions dans l'unificationGravatar herbelin2002-12-21
| | | | | | | faite par Rewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite du commit precedentGravatar barras2002-12-19
| | | | | | | | - 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
* nouveau Subst:Gravatar barras2002-12-17
| | | | | | | | - 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
* Traitement spécial pour les types à l'internalisationGravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3443 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du vernac Proof withGravatar gregoire2002-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)Gravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-ajout constrInGravatar herbelin2002-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3237 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - 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
* JMeq now treated as an equality by tactics.Gravatar courant2002-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3232 85f007b7-540e-0410-9357-904b9bb8a0f7
* Raffinement de l'heuristique d'unification dans sig_clausale_formeGravatar herbelin2002-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3218 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
| | | | | | | | | | | - 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
* Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et LocalGravatar herbelin2002-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3179 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-28 14:10:17 +0000