aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
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
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-04Confusion message erreur détectée par nouveau warning X de ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7509 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-10Petit bug Declare Implicit Tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7370 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Nouvelle déclaration 'Declare Implicit Tactic' pour automatiser la ↵herbelin
résolution des implicites restant après interprétation des termes dans les tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7363 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-08Réparation bug #1000 (attendre fin de toutes les intros avant d'effacer les ↵herbelin
'_' donnés dans le 'intros' (à cause des dépendances potentielles) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7355 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-08Réparation bug #1004; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7351 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13Correction double bug #986: Fold ne préserve pas nécessairement le typage ↵herbelin
et test de conversion buggé dans Logic.convert_hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7212 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-06essai de typage des instantiations d\'evarsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24New commit to allow definitions of morphisms on relations whose carrier issacerdot
a Prod. Example: m : feq ==> feq where m has type (A -> B) -> (C -> D) and few is a relation over (fun X Y: Type. X -> Y). The problem is to avoid the interpretation (A -> B) -> C -> D that tries to use feq over D and feq over C considering (A -> B) as a quantification. This closes a wish of Bas Spitters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7068 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵herbelin
reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Déplacement et export de locate_global (ex-locate_reference) de tacinterp ↵herbelin
vers syntax_def; Adoption du nom canonique global_of_constr pour éviter confusion avec type reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7050 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 01:34:33 +0000