aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2001-04-12Ajout de _ dans les patterns d'intromohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1584 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-12Mis un message d'erreur explicite pour l'echec de Elim en casmohring
d'incompatibilite de sortes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1581 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03Make it possible to perform proofs by induction even on non-inductive types,bertot
as long as one provides the induction principle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1522 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-22Problèmes de NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1477 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-09bug de refine: uncaught exception Array.subbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1443 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-08changement comparaison etatsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1436 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06Modification de e_give_exact pour eviter d'echouer sur l'unificationmohring
en l'absence de variables existentielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1431 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06eta-expansionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1430 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06EAutod (debug)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1429 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05module Explore générique et réécriture EAuto avec ce module; occur check ↵filliatr
dans clenv_merge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1425 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01backtrack unification types et deplacement make_clenv_bindingfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1417 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01nouvelle implantation de la reductionbarras
suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28modifmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1414 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-27EAuto mixte (largeur puis profondeur)mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1407 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26changement message d'erreur Abstractfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1405 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26Eauto version en largeurmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1404 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26Abstract: on échoue si le but contient des existentiellesfilliatr
(corrige un ug de EAuto with zarith) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1403 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16Prise en compte noms longs dans SuperAutoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1391 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en ↵herbelin
compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1388 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib ↵herbelin
(ex-Stdlib) et suppression Stock git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1386 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Bug affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1385 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib ↵herbelin
(ex-Stdlib) et suppression Stock git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1380 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1350 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06EqDecidefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1336 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Ajout d'une heuristique pour les types dependantsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1322 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Message d'erreur plus explicite pour Tautodelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1320 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05rétablissement nouveau Tautofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1318 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-03Résolution d'un bug de simplificationdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1317 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1308 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01oubli de Closure.EvalConstReffilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1305 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01- coqc : option -imagefilliatr
- coqmktop : manquaient des -I - tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau - correction d'un bug de Simpl avec Fix (découvert dans preuve FTA) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des ↵filliatr
constantes qualifiees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1301 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-30Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_mainsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1290 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-29As an heuristic, now both in tauto and intuition we try to avoid the initialsacerdot
reduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1287 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et ↵herbelin
réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1273 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et ↵herbelin
réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26On n'évite plus les globaux dans Intro, mais on les évite dans Abstractherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1220 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce ↵herbelin
dernier qui échouera si c'est pas normalisé de tête git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1218 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Command -> Constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1216 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Retrait du test d'existence "is_global" dans Intro ( fresh_id ) dherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1215 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Normalisation betaiota du pattern avant enregistrement comme hint (certains ↵herbelin
développements exploite cette caractéristique) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1214 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Bug confusion existS/sigSherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1210 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Command -> Constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1208 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Toujours Inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1178 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Toujours Inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1168 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-14 10:30:24 +0000