aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.mli
Commit message (Expand)AuthorAge
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
* (Port of r9984) Easier debugging:Gravatar glondu2007-07-12
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Extension to the general sequence operator (tactical). Now in addition to ...Gravatar emakarov2007-04-02
* affichage des ... dans les scriptsGravatar barras2006-10-16
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...Gravatar herbelin2004-12-31
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* Nouvelle en-têteGravatar herbelin2004-07-16
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* Amelioration de l'afficheur de script structureGravatar herbelin2003-11-05
* Ground Update.Gravatar corbinea2003-06-20
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* simplification de solve_subgoal: n'utilise plus frontierGravatar barras2002-12-19
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Réorganisation des tclTHEN (cf dev/changements.txt)Gravatar herbelin2002-05-29
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* Erreur dans un commentaire ...Gravatar clrenard2001-05-18
* entetesGravatar filliatr2001-03-15
* application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésGravatar filliatr2001-02-01
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Code redondantGravatar herbelin2000-10-13
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* DocGravatar herbelin2000-05-23
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* module PfeditGravatar filliatr1999-12-01
* - documentation repertoire proofs/Gravatar filliatr1999-10-20
* module RefinerGravatar filliatr1999-10-19
* les variables existentielles contiennent maintenant un environnement (typeGravatar filliatr1999-10-19
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18