aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2002-01-15Mise de Intros id au format de Intro en forçant aussi la réduction si demandéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2397 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-20Mise en place de la réduction sous forme d'implications d'atomes en fn de têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2356 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-20Utilisation de Hnf plutôt que Redherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2355 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Puisque Orelse semble lier moins que THEN, ajout d'un reduce après le Orelseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2352 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Insertion de Red sur chaque atome dans Tauto et Intuitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2347 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Tentative d'amélioration du résultat de Intuitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2340 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18coq-bugs #12: probleme de metamap resolubarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2308 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-06Parade contre effet indésirable du commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2277 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-06Amélioration nommage hypothèses NewInduction (et incompatibilités)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2275 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30desobfuscation du code de la verif de la condition de gardebarras
reparation bug de la tactique CutRewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2261 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Diverses petites simplications de la machine de preuves.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-13 19:20:29 +0000