aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extratactics.ml4
Commit message (Expand)AuthorAge
...
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Add a new tactic to generalize an instantiated inductive predicate adding equ...Gravatar msozeau2007-08-07
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* Ajout de la tactique "apply in".Gravatar herbelin2006-10-24
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
* Bug in replace tactics introduced in r9073 (overlap between replace .. with a...Gravatar jforest2006-08-23
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* Suite utilisation hyp au lieu ident: donne la localisationnGravatar herbelin2006-06-23
* Correction ident -> hyp pour dinterpréter des identificateurs devant êt...Gravatar herbelin2006-06-23
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Petit bug Declare Implicit TacticGravatar herbelin2005-09-10
* Nouvelle déclaration 'Declare Implicit Tactic' pour automatiser la résoluti...Gravatar herbelin2005-09-09
* Implemented autorewrite with ... in hyp [using ...].Gravatar sacerdot2005-05-18
* HUGE COMMITGravatar sacerdot2005-01-03
* Restauration type casted_open_constr pour tactique refine car l'unification n...Gravatar herbelin2004-12-09
* Uniformisation du nom d'entrée openconstr en le nom du type open_constrGravatar herbelin2004-12-06
* Déplacement de la coercion vis à vis du but au niveau de RefineGravatar herbelin2004-12-06
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...Gravatar herbelin2004-12-06
* Mise en conformité de Derive Inversion et Derive Dependent Inversion avec la...Gravatar herbelin2004-11-15
* Ajout 'dependent rewrite in'Gravatar herbelin2004-10-28
* Restructuration fonctions de réécriture depuis égalité dépendanteGravatar herbelin2004-10-27
* New commandsGravatar sacerdot2004-10-07
* * New syntactic sugar: Add Relation ... transitivity proved by ...Gravatar sacerdot2004-10-06
* The "Add Setoid" command now has a new argument "as name" that is usedGravatar sacerdot2004-10-01
* New tacticGravatar sacerdot2004-09-30
* New tactic [setoid_]rewrite ... in ... [generate side conditions ...].Gravatar sacerdot2004-09-30
* cutrewrite does not work with relations that are not Coq-like equalities.Gravatar sacerdot2004-09-30
* New syntaxGravatar sacerdot2004-09-29
* Hugly temporary notationGravatar sacerdot2004-09-29
* New: (temporary) concrete syntax to specify the morphism signature:Gravatar sacerdot2004-09-24
* Add_new_morphism has now a new optional argument that is the signature ofGravatar sacerdot2004-09-10
* New command "Add Relation ..." (for the new implementation of setoid_*).Gravatar sacerdot2004-09-03
* Setoid_replace.setoid_replace last argument (that was supposed to be alwaysGravatar sacerdot2004-07-23
* Nouvelle en-têteGravatar herbelin2004-07-16
* syntax compatibility fixGravatar corbinea2004-07-02
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* more evar stuffGravatar corbinea2004-06-28
* Backtrack sur commit 1.20Gravatar herbelin2004-03-18