aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2004-12-06Uniformisation du nom d'entrée openconstr en le nom du type open_constrherbelin
2004-12-06Garder les cast semble décidément le meilleur moyen de rester synchrone ave...herbelin
2004-12-06Suppression des cast après avoir utiliser l'information de type (Tacinv envo...herbelin
2004-12-06Déplacement de la coercion vis à vis du but au niveau de Refineherbelin
2004-12-06Déplacement de la coercion vis à vis du but au niveau de Refine suite à ch...herbelin
2004-12-06Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ...herbelin
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...herbelin
2004-12-06MAJ affichage nouvelle syntaxeherbelin
2004-12-04Bug 'set n in * |-'herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 04:35:16 +0000