aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
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
2006-02-23trying to fix a bug in pazrameter order in the multiple inductioncoq
tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8087 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17cleaningcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8054 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17bug correction in the decomposition of an induction scheme.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8053 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17changed the decomposition of an induction schemecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8052 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-16added isProd to term.mli.coq
added elim_scheme to tactics.mli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8049 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-15continuing the generalization of "induction". Now induction schemescoq
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
2006-02-10induction now admits multiple induction arguments. The principle mustcoq
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
2006-02-05Debugging en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7991 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Ajout option 'using lemmas' à auto/trivial/eautoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7937 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Suppression code pour hints nommés à la V7 (voire à la V6...)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7936 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-24Suppression de la dépendance en Map.fold de ocaml dont la sémantique aherbelin
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
2006-01-21Messages de idtac et fail peuvent maintenant être des listes de string, int ↵herbelin
et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7909 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et ↵herbelin
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
2006-01-21Backtrack commit précédent (incompatible avec le choix de prendre Idtac ↵herbelin
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
2006-01-20Ajout de la contrainte de résoudre l'assertion dans 'assert by'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7902 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Conséquences supplémentaires de la fin du support v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7895 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Export eassumptionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7894 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coqherbelin
choisir un nom; utilisation de IntroAnonymous au lieu de None dans l'argument "with_names" des tactiques induction, inversion et assert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7880 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Code redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7877 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16- Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesherbelin
- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns - TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7841 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7839 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Résidus du traducteur v7 -> v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7835 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Nettoyage coqlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7759 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Petite correction nom QuantHypArgType suite suppression traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7739 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Prise en compte de l'information que certaines tactiques attendent un type ↵herbelin
(utile pour coercions et interpretation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7683 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de ↵herbelin
tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7681 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-17A la demande de Julien Forestletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7573 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 18:39:18 +0000