aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2006-09-23Correction bug #1229 (toplevel "unresolved evar" fled throughherbelin
Declare Implicit Tactic support) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9165 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-22Ajout d'une valeur VList dans tacinterp pour permettre de cabler desherbelin
Tactic Notation acceptant des listes en entrée avec application à la définition de revert dans Tactics.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9159 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-21Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter ↵herbelin
sans ouverture, comme c'est le cas pour les autres Hints git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9157 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-20Declarative Proof Language: main commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-12Indentation + svnpropnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9133 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Correction bug d'ordonnancement des hyps d'induction dans induction/destructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9119 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28improve the amount of information given by the Ltac tactic debuggerbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9092 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-23Bug in replace tactics introduced in r9073 (overlap between replace .. with ↵jforest
and replace_term). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9076 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22Forgot a file in previous commit jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9074 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-17corrects an error in the substitution of module paths inside tactics:bertot
objects of the form TacDynamic should not be left unchanged if their content is tagged with "constr". This correction makes that setoid ring can now work with rings that were declared inside a module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9070 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-28Reparation bug Show intros: les hypothèses introduites précédemmentcourtieu
dans le même paquet doivent être typables pour décider le nom des suivantes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9061 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-20Correction du bug #1116 jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9057 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-18amelioration du comportement de induction (retour a la version V8.0)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9056 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Correcting for bug #1167 jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9010 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-27Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans ↵herbelin
l'environnement de preuve au moment de l'interprétation des arguments de tactiques (version 8971) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8991 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Suite utilisation hyp au lieu ident: donne la localisationnherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8979 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Correction ident -> hyp pour dinterpréter des identificateurs devant ↵herbelin
être interprétés comme termes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8977 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Préservation compatibilité interprétation quantified hypothesis ↵herbelin
(provisoire ?) + export nouvelle macro pour maple.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8975 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Nettoyage, uniformisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8971 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-21Harmonisation de l'interprétation des intropatternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8967 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-19bug serieux efficacite de ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8963 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-12Updating documentation of replace and correcting a typo in error message of ↵jforest
replace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8950 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Changement du type d'argument 'TacticArgType X' en un typeherbelin
'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de pouvoir typer correctement les wit_tactic (auparavant le typage des wit_tactic était trop libéral et permettait de casser la subject-reduction). Amélioration au passage de l'affichage de la tactique "replace by" (module Extratactics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06reparation pour le bug #1072 (soufflee par J. Forest): letouzey
protection d'un list_chop pour couvrir le cas d'une application partielle de morphisme. accessoirement, il faudrait comprendre un jour pourquoi setoid replace inspecte (and True) dans le terme (map (and True) True <-> A) si on lui dit de reecrire A en autre chose... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8900 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour ↵herbelin
permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
- prise en compte du niveau à la déclaration du type comme une fonction des sortes des conclusions des paramètres uniformes - suppression du retypage de chaque instance de type inductif (trop coûteux) et donc abandon de l'idée de calculer une sorte minimale même dans des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-20"subst." works now even when it exists an hypothesis have the form "x=x" in ↵jforest
the goal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8835 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-05encore un correctif sur le rewrite H in setoid: letouzey
si H: a==b, alors ce rewrite echouait lorsque a apparait dans b ou b dans a. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8788 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-02Extension syntaxique de rewrite in: au lieu de pouvoir faire letouzey
juste rewrite in <id>, on a maintenant rewrite in <clause>. Ainsi rewrite H in H1,H2 |- * === rewrite H in H1; rewrite H in H2; rewrite H Pour l'instant rewrite H in * |- signifie: faire une fois "try rewrite H in Hi" sur toutes les hypotheses Hi du contexte sauf H En particulier, n'echoue pour l'instant pas s'il n'y a rien a reecrire nulle part. NB: rewrite H in * === rewrite H in * |- * === rewrite H in * |- ; rewrite H ATTENTION: la syntaxe de rewrite ayant changé, j'adapte interface en conséquence. Est-ce la bonne facon de faire ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8780 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-02Changement de comportement de rewrite: face a une egalité setoid, onletouzey
arrete de reduire brutalement pour essayer de tomber sur une egalité Coq. Au contraire, si la relation de tete est une relation declarée dans la base des setoids, on l'utilise. ATTENTION: ceci brise la compatibilité, dans le cas très improbable ou quelqu'un aurait defini un setoid mais exploiterait la "feature" de la reduction vers l'eventuelle egalité Coq sous-jacente. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8779 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-02Correction bug du correctif bug assert asherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8778 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-02Bug assert asherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8774 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Standardisation du nom des méthodes de Evdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Diverses corrections de l'afficheur et du traducteur pour s'assurer deherbelin
la réversibilité de la traduction (correction enregistrement des retours chariot dans le lexeur, correction affichage espace superflu en tête des VERNAC EXTEND, correction affichage morphism_signature dans extraargs.ml4, correction affichage clear dans pptactic.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8739 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-12induction on multiple arguments made better:courtieu
- dealing with arguments depending one on another - cleaning letins created during induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8701 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-11adding a new tactic [intro_avoiding idl] which acts as intro but prevents thejforest
new identifier to bellong to [idl] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8698 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-06Enlevement de message d'erreur garbage.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8684 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses letouzey
avec des equivalences parametrees (genre forall n, P n <-> Q n) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8683 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05ajout d'un rattrapage d'erreur pour "induction using".courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8679 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-02Correction bug 1119 (inversion marche a moitie dans Type)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8677 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default ↵msozeau
uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deherbelin
la compilation de fichiers comme hipattern.ml (renommé en hipattern.ml4) - Extension de eqdecide.ml4 pour qu'il gère les buts sans quantificateurs, basés soient sur sumbool soit sur or, et à symétrie près de la disjunction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8652 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-21+ destruct now works as induction on multiple arguments : jforest
destruct x y z using scheme + replace c1 with c2 <in hyp> has now a new optional argument <as tac> replace c1 with c2 by tac tries to prove c2 = c1 with tac + I've also factorize the code correspoing to replace in extractactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8651 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-12 -Debugging multiple induction, a bug appeared when having functioncourtieu
arguments to a principle (like in map_ind). -Added nbranches and npredicates to elim_scheme, and made the elimc field optional. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8622 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une ↵herbelin
référence explicitement de ltac + nettoyage unrec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8128 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-02Correction bug #1097 (dû à une typo...)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8114 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:59:46 +0000