aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2005-05-18Implemented autorewrite with ... in hyp [using ...].sacerdot
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-05-15Globalisation des Tactic Notationherbelin
2005-05-15Allow auto to have a parametric argument (wish #967)herbelin
2005-04-29Improved order of interpretation of atomic tactics (cf bug #952)herbelin
2005-03-22Ajout de l'axiome du but prouve par la tactique simplificoq
2005-03-20Correction bug de dependent_hyps qui ne met pas à jour le type des hyps dép...herbelin
2005-03-19Le type d'un Let est considéré comme 'user-provided' par le noyau et doit d...herbelin
2005-03-19Report depuis la V8.0pl2 de la correction d'un bug du traducteurherbelin
2005-03-18appel de Simplify depuis Coqcoq
2005-03-08Fix bug #931: leave dependent evars as such for refineherbelin
2005-03-07Added 'clear - id' to clear all hypotheses except the ones dependent in the s...herbelin
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse in...herbelin
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse in...herbelin
2005-02-04Ajout constructeur External pour appel outil externe à Coqherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-18Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of thesacerdot
2005-01-17Bug fixed (reported by Roland): the setoire_rewrite in tactic did not worksacerdot
2005-01-03HUGE COMMITsacerdot
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...herbelin
2004-12-29ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...herbelin
2004-12-09Restauration type casted_open_constr pour tactique refine car l'unification n...herbelin
2004-12-07* added subst_evaluable_referencesacerdot
2004-12-07The type Pattern.constr_label was isomorphic to Libnames.global_reference.sacerdot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 20:50:57 +0000