aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2001-11-12Suppression des stamps et donc des *_constraintsclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06Suite de la suppression : enamed_declaration est remplace par evar_map.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2164 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-23Bug Induction (prise en compte let-in + ordre des dépendances dans thin)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2134 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-15Export hide_ident_or_numarg_tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2119 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-15Prise en compte Intros until dans Discriminate, Injection et Simplify_eq + ↵herbelin
nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2116 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-10Incompatibilité entre la prise en compte des univers au niveau des ↵herbelin
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
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs ↵herbelin
'ClearBody H' et 'Assert H := c' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-30Ajout du printer de tactiques + modif du Dynamic ocamldelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2086 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21make docfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2041 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Correction (double) bug de Generalize Dependentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2037 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20let-in dans Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2013 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵herbelin
des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Deplacement des setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Modification de l'emplacement des fichiers pour les setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14Ajout syntaxe "Assert H:T."herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1968 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-13eclaircissement du codecourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1957 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵herbelin
é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
2001-09-09Nettoyage reduce_to_ind et one_step_reduceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1942 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1938 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-03Correction d'un bug de pretty-print.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1919 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-28Change la constante d'entree de Immediatemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1901 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Parsingherbelin
- 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
2001-08-08Renommage TrueCut -> Assertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1887 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08La grammaire n'était plus LL1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1885 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08Modification Tauto pour qu'il puisse destructurer des hypotheses de la formecourant
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
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ↵herbelin
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
2001-08-05Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas ↵herbelin
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
2001-08-05Elimination des coupures quand les 'clause' se réduisent à des ↵herbelin
hypothèses, nouveau combinateur onHyps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1877 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas ↵herbelin
s'appliquer au but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1875 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Mise en place d'un nouveau Destruct sur le modèle du nouvel Inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1874 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Suppression des TmpHyp disgracieuses dans Decompose; utilisation de ↵herbelin
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
2001-08-05Elimination des coupures quand les 'clause' se réduisent à des ↵herbelin
hypothèses, nouveau combinateur onHyps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1872 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-01Ajout code pour un Destruct similaire au NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1870 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-13Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne ↵herbelin
prend pas les letin en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1848 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Branchement sur bad_tactic_argsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1846 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Branchement sur bad_tactic_argsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1845 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout du .ml pour la tactique Setoid_replaceclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1843 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Changement de place de la tactique Setoid_rewrite et renommageclrenard
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
2001-07-04ajout Show Intro(s)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1825 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-29Autoriser Apply avec un but sous forme d'implication ou de quantificationbarras
universelle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1817 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-29traitement du let dans red_product (tactique Red)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1815 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-27commit d'un bug de Apply.barras
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
2001-06-25Refine sur les CoFixfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1807 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 17:45:04 +0000