aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of theGravatar sacerdot2005-01-18
* Bug fixed (reported by Roland): the setoire_rewrite in tactic did not workGravatar sacerdot2005-01-17
* HUGE COMMITGravatar sacerdot2005-01-03
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...Gravatar herbelin2004-12-29
* Restauration type casted_open_constr pour tactique refine car l'unification n...Gravatar herbelin2004-12-09
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
* The type Pattern.constr_label was isomorphic to Libnames.global_reference.Gravatar sacerdot2004-12-07
* Uniformisation du nom d'entrée openconstr en le nom du type open_constrGravatar herbelin2004-12-06
* Garder les cast semble décidément le meilleur moyen de rester synchrone ave...Gravatar herbelin2004-12-06
* Suppression des cast après avoir utiliser l'information de type (Tacinv envo...Gravatar herbelin2004-12-06
* Déplacement de la coercion vis à vis du but au niveau de RefineGravatar herbelin2004-12-06
* Déplacement de la coercion vis à vis du but au niveau de Refine suite à ch...Gravatar herbelin2004-12-06
* Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ...Gravatar herbelin2004-12-06
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...Gravatar herbelin2004-12-06
* MAJ affichage nouvelle syntaxeGravatar herbelin2004-12-06
* Bug 'set n in * |-'Gravatar herbelin2004-12-04
* backtrack of the last commit (it was my fault: the code is used byGravatar sacerdot2004-11-26
* unused function in the interfaceGravatar sacerdot2004-11-26
* Réparation incompatibilité de comportement introduite lors de mise en compa...Gravatar herbelin2004-11-22
* Expansion Case dans injection et discriminate (cf bug #829)Gravatar herbelin2004-11-21
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Mise en conformité de Derive Inversion et Derive Dependent Inversion avec la...Gravatar herbelin2004-11-15
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Added code to get rid of duplicate rewriting rules.Gravatar sacerdot2004-10-28
* Ajout 'dependent rewrite in'Gravatar herbelin2004-10-28
* Factorisation cut_replacingGravatar herbelin2004-10-27
* Restructuration fonctions de réécriture depuis égalité dépendanteGravatar herbelin2004-10-27
* Restructuration fonctions de réécriture depuis égalité dépendante; facto...Gravatar herbelin2004-10-27
* Word "setoid" banned from the error messages. "relation" used instead.Gravatar sacerdot2004-10-25
* Missing check implemented (closes a bug from Bas Spitters).Gravatar sacerdot2004-10-25
* The morphism lemma type was simplified only in modules and not in moduleGravatar sacerdot2004-10-21
* Error message improved.Gravatar sacerdot2004-10-21
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* The bug already closed in revision 1.90 was reintroduced again.Gravatar sacerdot2004-10-20
* Proof term size reduction (again).Gravatar sacerdot2004-10-19
* * Code simplification and clean-up. In particular there is no more codeGravatar sacerdot2004-10-18
* Code simplification and clean-up.Gravatar sacerdot2004-10-18
* The lem field was not computed properly for morphisms whose argument wasGravatar sacerdot2004-10-18
* The "lem" field of a morphism used to be the compatibility proof, but itGravatar sacerdot2004-10-18
* Bug fixed: relations quantified more than once where abstracted in the wrongGravatar sacerdot2004-10-18
* More informative error message when the tactic tries to generate a newGravatar sacerdot2004-10-18
* zeta flag added to reduce LetIns in a morphism type. Morphisms with localGravatar sacerdot2004-10-18
* Wrong comment committed. The tactic behaves correctly only when theGravatar sacerdot2004-10-15
* Wish of Maggesi implemented: the type of the morphism compatibility lemmaGravatar sacerdot2004-10-15
* Bug fixed (reported by Maggesi): sometimes when the tactic had to generate newGravatar sacerdot2004-10-14
* Code clean-up.Gravatar sacerdot2004-10-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 08:25:32 +0000