aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2005-05-24New commit to allow definitions of morphisms on relations whose carrier issacerdot
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-05-20Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...herbelin
2005-05-19Setoid_replace: improved error message when trying to replace a term in asacerdot
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 18:08:05 +0000