aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans ↵Gravatar herbelin2006-06-27
| | | | | | 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
* Suite utilisation hyp au lieu ident: donne la localisationnGravatar herbelin2006-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8979 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction ident -> hyp pour dinterpréter des identificateurs devant ↵Gravatar herbelin2006-06-23
| | | | | | être interprétés comme termes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Préservation compatibilité interprétation quantified hypothesis ↵Gravatar herbelin2006-06-23
| | | | | | (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
* Nettoyage, uniformisationGravatar herbelin2006-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Harmonisation de l'interprétation des intropatternGravatar herbelin2006-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8967 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug serieux efficacite de ltacGravatar barras2006-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8963 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating documentation of replace and correcting a typo in error message of ↵Gravatar jforest2006-06-12
| | | | | | replace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
| | | | | | | | | | | | | | '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
* reparation pour le bug #1072 (soufflee par J. Forest): Gravatar letouzey2006-06-06
| | | | | | | | | | | | | 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
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour ↵Gravatar herbelin2006-05-30
| | | | | | 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
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
| | | | | | | | | | | 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
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
| | | | | | | | | | | - 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
* "subst." works now even when it exists an hypothesis have the form "x=x" in ↵Gravatar jforest2006-05-20
| | | | | | the goal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8835 85f007b7-540e-0410-9357-904b9bb8a0f7
* encore un correctif sur le rewrite H in setoid: Gravatar letouzey2006-05-05
| | | | | | | | | 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
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
| | | | | | | | | | | | | | | | | | | | | 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
* Changement de comportement de rewrite: face a une egalité setoid, onGravatar letouzey2006-05-02
| | | | | | | | | | | | | | 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
* Correction bug du correctif bug assert asGravatar herbelin2006-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8778 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug assert asGravatar herbelin2006-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵Gravatar notin2006-04-28
| | | | | | 'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses corrections de l'afficheur et du traducteur pour s'assurer deGravatar herbelin2006-04-26
| | | | | | | | | | 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
* induction on multiple arguments made better:Gravatar courtieu2006-04-12
| | | | | | | - 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
* adding a new tactic [intro_avoiding idl] which acts as intro but prevents theGravatar jforest2006-04-11
| | | | | | | new identifier to bellong to [idl] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8698 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enlevement de message d'erreur garbage.Gravatar courtieu2006-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8684 85f007b7-540e-0410-9357-904b9bb8a0f7
* resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses Gravatar letouzey2006-04-05
| | | | | | | | 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
* ajout d'un rattrapage d'erreur pour "induction using".Gravatar courtieu2006-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1119 (inversion marche a moitie dans Type)Gravatar herbelin2006-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made pretyping a functor over a coercion implementation. Pretyping.Default ↵Gravatar msozeau2006-03-22
| | | | | | | | | | | 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
* - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deGravatar herbelin2006-03-22
| | | | | | | | | | | 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
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
| | | | | | | | | | | 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
* -Debugging multiple induction, a bug appeared when having functionGravatar courtieu2006-03-12
| | | | | | | | | | 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
* Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une ↵Gravatar herbelin2006-03-05
| | | | | | 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
* Correction bug #1097 (dû à une typo...)Gravatar herbelin2006-03-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8114 85f007b7-540e-0410-9357-904b9bb8a0f7
* trying to fix a bug in pazrameter order in the multiple inductionGravatar coq2006-02-23
| | | | | | | tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8087 85f007b7-540e-0410-9357-904b9bb8a0f7
* cleaningGravatar coq2006-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8054 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug correction in the decomposition of an induction scheme.Gravatar coq2006-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8053 85f007b7-540e-0410-9357-904b9bb8a0f7
* changed the decomposition of an induction schemeGravatar coq2006-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8052 85f007b7-540e-0410-9357-904b9bb8a0f7
* added isProd to term.mli.Gravatar coq2006-02-16
| | | | | | | added elim_scheme to tactics.mli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8049 85f007b7-540e-0410-9357-904b9bb8a0f7
* continuing the generalization of "induction". Now induction schemesGravatar coq2006-02-15
| | | | | | | | | | | | | | | | with multiple args AND no main induction arg can be used directly with induction. The last functional argument is not necessary anymore. For example: nat_double_ind: forall R : nat -> nat -> Prop, ...branches... -> forall n m : nat, R n m. is ok. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8046 85f007b7-540e-0410-9357-904b9bb8a0f7
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
| | | | | | | | | | | | | be explicitely given, and ALL parameters and args of the scheme must be given (only branches must be omitted). For the moment, only principle like generated by GenFixpoint (functional induction) are usable. That is the predicate must have a additional paramter like in: (P x1 ... xn (f p1...pm x1...xn)) Example of use : induction x y (add x y) using add_ind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debugging en syntaxe v8Gravatar herbelin2006-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7937 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
| | | | | | | | changé entre les version 3.08.4 et 3.09.0 (influe notamment sur l'ordre d'application des Hints de auto) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7925 85f007b7-540e-0410-9357-904b9bb8a0f7
* Messages de idtac et fail peuvent maintenant être des listes de string, int ↵Gravatar herbelin2006-01-21
| | | | | | et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7909 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et ↵Gravatar herbelin2006-01-21
| | | | | | fail peuvent maintenant être des listes de string, int et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack commit précédent (incompatible avec le choix de prendre Idtac ↵Gravatar herbelin2006-01-21
| | | | | | comme défaut pour ne rien faire) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7906 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 21:07:30 +0000