aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Uniformisation des politiques de nommage de NewDestruct sur arguments ↵Gravatar herbelin2003-11-25
| | | | | | recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵Gravatar herbelin2003-11-24
| | | | | | passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug introduit avec le 'Simpl f'Gravatar herbelin2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Blindage vis a vis des constructeurs partiellement appliquesGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4937 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tactics : econstructor, eleft, eright, esplitGravatar clrenard2003-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug nommage destructGravatar herbelin2003-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4922 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robusteGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4916 85f007b7-540e-0410-9357-904b9bb8a0f7
* factorisation et generalisation des clausesGravatar barras2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des alias syntaxiques vers des references dans divers lieux ↵Gravatar herbelin2003-11-12
| | | | | | de globalisation des constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits changements de syntaxeGravatar barras2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction semantique des InHyp de clause en InHypValue si local defGravatar herbelin2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction semantique des InHyp de clause en InHypValue si local def; ↵Gravatar herbelin2003-11-09
| | | | | | simplification suite fusion eq/eqT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4840 85f007b7-540e-0410-9357-904b9bb8a0f7
* 'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ↵Gravatar herbelin2003-11-09
| | | | | | de Generalize Dependent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4834 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code obsoleteGravatar herbelin2003-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4833 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2003-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4830 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Instantiate ... inGravatar corbinea2003-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration message d'erreur avec pretyping; prise en compte syntactic def ↵Gravatar herbelin2003-11-04
| | | | | | dans Unfold git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug Double InversionGravatar herbelin2003-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4719 85f007b7-540e-0410-9357-904b9bb8a0f7
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
| | | | | | | Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec ↵Gravatar herbelin2003-10-21
| | | | | | alpha-conversion et seulement apres avec conversion (suggestion de Carlos Simpson) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug FreshIdGravatar herbelin2003-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Globalisation des hints autorewriteGravatar herbelin2003-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de l'utilisation de contradictionGravatar herbelin2003-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Contradiction au cas d'hypotheses ~A et A dans le contexteGravatar herbelin2003-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4673 85f007b7-540e-0410-9357-904b9bb8a0f7
* subst marche dans les deux sensGravatar filliatr2003-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4663 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle syntaxe de ltacGravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un Try supplementaire utile pour la compatibilite, car bring_hyps dans ↵Gravatar herbelin2003-10-13
| | | | | | generalizeRewriteIntros peut echouer (typage) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation comportement decompEq pour corriger un bug introduit dans le ↵Gravatar herbelin2003-10-11
| | | | | | Inversion acceptant le nommage des hypotheses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug calcul du nom de la premiere equationGravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Death of 'a somewhat cryptic module'Gravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Death of 'a somewhat cryptic module'Gravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4596 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dead of 'a somewhat cryptic module'Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; ↵Gravatar herbelin2003-10-10
| | | | | | pf_get_new_id moved to Tacmach) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification lemInv et lemInv_inGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4568 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cablage en dur de inversionGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4565 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage des buts par Pfedit pour utilisation par les tactiques ↵Gravatar herbelin2003-10-10
| | | | | | (Setoid_replace) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4562 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug utilisation nametab pour ltacGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4550 85f007b7-540e-0410-9357-904b9bb8a0f7
* Des abbreviations pour constrintern.ml; generic argument IdentArgGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4547 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug NewInduction pour les inductifs de type 'ordinaux'Gravatar herbelin2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug internalisation des Extern: la globalisation doit etre stricteGravatar herbelin2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4453 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à la V8 par défautGravatar herbelin2003-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interface EautoGravatar herbelin2003-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4415 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 16:49:13 +0000