aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Incompatibilité entre la prise en compte des univers au niveau des ↵Gravatar herbelin2001-10-10
| | | | | | tactiques et le test de conversion qui oublie la cumulativité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs ↵Gravatar herbelin2001-10-05
| | | | | | 'ClearBody H' et 'Assert H := c' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du printer de tactiques + modif du Dynamic ocamlGravatar delahaye2001-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2086 85f007b7-540e-0410-9357-904b9bb8a0f7
* make docGravatar filliatr2001-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction (double) bug de Generalize DependentGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2037 85f007b7-540e-0410-9357-904b9bb8a0f7
* TransparentGravatar barras2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
* let-in dans RefineGravatar filliatr2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵Gravatar herbelin2001-09-19
| | | | | | des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement des setoides.Gravatar clrenard2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de l'emplacement des fichiers pour les setoides.Gravatar clrenard2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout syntaxe "Assert H:T."Gravatar herbelin2001-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1968 85f007b7-540e-0410-9357-904b9bb8a0f7
* eclaircissement du codeGravatar courant2001-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵Gravatar herbelin2001-09-10
| | | | | | éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage reduce_to_ind et one_step_reduceGravatar herbelin2001-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Préparation à la mise en place d'univers algébriquesGravatar herbelin2001-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1938 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug de pretty-print.Gravatar clrenard2001-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1919 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change la constante d'entree de ImmediateGravatar mohring2001-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1901 85f007b7-540e-0410-9357-904b9bb8a0f7
* ParsingGravatar herbelin2001-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage TrueCut -> AssertGravatar herbelin2001-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1887 85f007b7-540e-0410-9357-904b9bb8a0f7
* La grammaire n'était plus LL1Gravatar herbelin2001-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1885 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification Tauto pour qu'il puisse destructurer des hypotheses de la formeGravatar courant2001-08-08
| | | | | | | | e1 -> e2 avec e1 type inductif ayant un unique constructeur constant. Cas typique : hypothese de la forme ~e=e. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ↵Gravatar herbelin2001-08-07
| | | | | | tactique primitive Cut basé sur un Let non dépendant; amélioration efficacité ancien Cut git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas ↵Gravatar herbelin2001-08-05
| | | | | | s'appliquer au but; appel optionnel de Intros Until sur certaines tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1878 85f007b7-540e-0410-9357-904b9bb8a0f7
* Elimination des coupures quand les 'clause' se réduisent à des ↵Gravatar herbelin2001-08-05
| | | | | | hypothèses, nouveau combinateur onHyps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas ↵Gravatar herbelin2001-08-05
| | | | | | s'appliquer au but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1875 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un nouveau Destruct sur le modèle du nouvel InductionGravatar herbelin2001-08-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des TmpHyp disgracieuses dans Decompose; utilisation de ↵Gravatar herbelin2001-08-05
| | | | | | combinateurs sur les hyps plutôt que sur les clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Elimination des coupures quand les 'clause' se réduisent à des ↵Gravatar herbelin2001-08-05
| | | | | | hypothèses, nouveau combinateur onHyps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout code pour un Destruct similaire au NewInductionGravatar herbelin2001-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne ↵Gravatar herbelin2001-07-13
| | | | | | prend pas les letin en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Branchement sur bad_tactic_argsGravatar herbelin2001-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Branchement sur bad_tactic_argsGravatar herbelin2001-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1845 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du .ml pour la tactique Setoid_replaceGravatar clrenard2001-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1843 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de place de la tactique Setoid_rewrite et renommageGravatar clrenard2001-07-10
| | | | | | | | en Rewrite. Le choix entre egalite de Leibnitz et egalite de setoide est fait automatiquement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1841 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout Show Intro(s)Gravatar letouzey2001-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Autoriser Apply avec un but sous forme d'implication ou de quantificationGravatar barras2001-06-29
| | | | | | | universelle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1817 85f007b7-540e-0410-9357-904b9bb8a0f7
* traitement du let dans red_product (tactique Red)Gravatar barras2001-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1815 85f007b7-540e-0410-9357-904b9bb8a0f7
* commit d'un bug de Apply.Gravatar barras2001-06-27
| | | | | | | | | | Avec Apply c, on essaie d'unifier le type de c avec le but courant. Si ca echoue on essaie d'expanser la constante de tete du type du theoreme, et essaie de faire Apply recursivement. Ca ameliore sensiblement la puissance de Apply mais ce n'est pas 100% backward-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1814 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refine sur les CoFixGravatar filliatr2001-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵Gravatar herbelin2001-06-25
| | | | | | définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵Gravatar herbelin2001-06-25
| | | | | | compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix d'un bug de TautoGravatar delahaye2001-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte env local (et defs locales) dans ChangeGravatar herbelin2001-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug du a un Intros trop violentGravatar delahaye2001-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1777 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ↵Gravatar herbelin2001-06-01
| | | | | | des variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1776 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration - subjective - de l'affichage des HintGravatar herbelin2001-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pretty -> PrettypGravatar filliatr2001-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_typesGravatar herbelin2001-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1762 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
| | | | | | | ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 01:17:18 +0000