aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2006-03-22- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deherbelin
2006-03-21+ destruct now works as induction on multiple arguments : jforest
2006-03-12 -Debugging multiple induction, a bug appeared when having functioncourtieu
2006-03-05Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...herbelin
2006-03-02Correction bug #1097 (dû à une typo...)herbelin
2006-02-23trying to fix a bug in pazrameter order in the multiple inductioncoq
2006-02-17cleaningcoq
2006-02-17bug correction in the decomposition of an induction scheme.coq
2006-02-17changed the decomposition of an induction schemecoq
2006-02-16added isProd to term.mli.coq
2006-02-15continuing the generalization of "induction". Now induction schemescoq
2006-02-10induction now admits multiple induction arguments. The principle mustcoq
2006-02-05Debugging en syntaxe v8herbelin
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
2006-01-28Ajout option 'using lemmas' à auto/trivial/eautoherbelin
2006-01-28Suppression code pour hints nommés à la V7 (voire à la V6...)herbelin
2006-01-24Suppression de la dépendance en Map.fold de ocaml dont la sémantique aherbelin
2006-01-21Messages de idtac et fail peuvent maintenant être des listes de string, int ...herbelin
2006-01-21Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...herbelin
2006-01-21Backtrack commit précédent (incompatible avec le choix de prendre Idtac com...herbelin
2006-01-20Ajout de la contrainte de résoudre l'assertion dans 'assert by'herbelin
2006-01-19Conséquences supplémentaires de la fin du support v7herbelin
2006-01-19Export eassumptionherbelin
2006-01-16Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coqherbelin
2006-01-16Code redondantherbelin
2006-01-16- Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesherbelin
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
2006-01-11Résidus du traducteur v7 -> v8herbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
2005-12-30Nettoyage coqlibherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Petite correction nom QuantHypArgType suite suppression traducteurherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-21Prise en compte de l'information que certaines tactiques attendent un type (u...herbelin
2005-12-21Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-17A la demande de Julien Forestletouzey
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-04Confusion message erreur détectée par nouveau warning X de ocaml 3.09herbelin
2005-11-02Types inductifs parametriquesmohring
2005-09-10Petit bug Declare Implicit Tacticherbelin
2005-09-09Nouvelle déclaration 'Declare Implicit Tactic' pour automatiser la résoluti...herbelin
2005-09-08Réparation bug #1000 (attendre fin de toutes les intros avant d'effacer les ...herbelin
2005-09-08Réparation bug #1004; nettoyageherbelin
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
2005-07-13Correction double bug #986: Fold ne préserve pas nécessairement le typage e...herbelin
2005-06-06essai de typage des instantiations d\'evarsbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:04:09 +0000