aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eauto.ml4
Commit message (Expand)AuthorAge
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Suite unification apply et eapply (l'un et l'autre profite maintenantGravatar herbelin2007-04-16
* Essai de partage de code entre apply et eapplyGravatar herbelin2007-04-15
* Correction d'une tentative incorrecte (révision 9266) de clarificationGravatar herbelin2006-10-25
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Debugging en syntaxe v8Gravatar herbelin2006-02-05
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* Export eassumptionGravatar herbelin2006-01-19
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...Gravatar herbelin2005-12-21
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Nouvelle tactique EExistsGravatar clrenard2003-12-01
* New tactics : econstructor, eleft, eright, esplitGravatar clrenard2003-11-17
* NettoyageGravatar herbelin2003-11-08
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...Gravatar herbelin2002-06-05
* Fichiers tactics/*.ml4 remplacent les tactics/*.vGravatar herbelin2002-05-29