aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2002-07-17tactique Substfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2894 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-17Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3|- ?]corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2893 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Bug dans la globalisation des arguments de tactiques primitivesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2882 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15Correction bug Tauto : la regle pour (A->B)->C echouait quand C etaitcourant
de la forme (E->F)->G. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2868 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Que la localisation des erreurs pour les tactiques atomiques marcheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2853 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-03Hack pour autoriser les $n dans les Grammar tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2837 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-13Réparation de l'interprétation des fermetures (sans casser Field!)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2779 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout coercion constr vers hyp quantifiéeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2765 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Tentative de réparation d'un bug Omega: une variable de section qui après ↵herbelin
effacement ne peut être renommée pareille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2763 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Passage de PatternMatchingFailure vers UserError pour capture par tclFIRSTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Repercussion de la possibilit de mettre des hyps quantifiees dans ↵herbelin
Simplify_eq et Injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2757 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq ↵herbelin
et Injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2754 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; ↵herbelin
rparation de la protection contre les clauses indiscernables de TACTIC EXTEND et VERNAC COMMAND EXTEND; rparation des grammaires de Extraction, EAuto, TextMode, KillProof et Derive Dependent Inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2753 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-31Les VContext ne sont plus des fermetures (temporaire)delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2743 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-30Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2737 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2735 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2724 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Réorganisation des tclTHEN (cf dev/changements.txt)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2721 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2719 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Pour les tactiques dépendant de Falseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2718 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-22Correction of a bug in Intuition (no more decomposition of dependent pairs).corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2704 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
gauche à droite des hypothèses dans Intuition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2696 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Finalement VTactic est gardé pour y plonger les tactiques ML, leherbelin
VTactic utilisé pour les fermetures de ltac s'appelle maintenant VTacticClos git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2693 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14- Changement de l'ordre de filtrage dans "Match Context"herbelin
- Protection des "Match Context" contre les exceptions non UserError ni Fail - Remplacement des fermetures ML dans VTactic et VFTactic par des expressions de tactiques pour permettre l'intégration de Tactic Definition dans les états - Changement en conséquence de Tauto git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2685 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewritebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2680 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14Changement de eq en eqT comme equivalence de setoide par defaut.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2679 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-02Minor correction of get_lem_namecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2664 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-02nettoyage codecourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2663 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-11Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2632 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2618 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-27Simplification de Proof_type.prim_ruleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2571 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-26Prise en compte des dependances dans la tactique Casemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2567 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-21Intuition ne fait plus de Unfold des constantes (il faut les fairecourant
soi-même si nécessaire) : l'idée est d'avoir un comportement clair et toujours aussi rapide que possible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2559 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-20Intuition now takes an (optional) tactic as parameter. This tactic iscourant
used to solve the goal remaining after propositional destructuration of the goal and the hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2554 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-15Tauto est maintenant stable par "Intro" :courant
Tauto montre (x:nat)(P x) |- (x:nat)(P x) aussi bien que |- (x:nat)(P x)->(P x) Intuition aussi. De plus, Intuition résout maintenant tout ce que Tauto sait résoudre ; par exemple (A,B,C:Prop)A\/(B/\C->C/\B) (ce qui n'était pas le cas jusqu'ici). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2533 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-13*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2528 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-07Simplify_eq echouait sur des hypotheses trivial comme O=Obarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2518 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2516 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05assert failure avec Conditional Rewritebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2513 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05suppression de code mortbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2510 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Nouveau Rewrite-in plus economiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-01labels appliques dans un ordre incorrectbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2504 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28Uniformisation convert_hyp; correction problème de dépendance dans letin_tacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2501 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-22suppression de pop_namedbarras
meilleure discrimination dans les tactiques d'inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-19Elim dependente n'appelait pas la bonne fonction pour calculer le predicatbarras
d'elimination (d'ou le bug avec Dependent Inversion) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2484 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-18but de CutRewrite <- (assert false)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2482 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15petits changements cosmetiques sur les tactiquesbarras
+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 10:33:44 +0000