aboutsummaryrefslogtreecommitdiff
path: root/proofs/refiner.mli
AgeCommit message (Expand)Author
2003-11-12Idtac peut prendre un argument à affichernarboux
2003-11-05Amelioration de l'afficheur de script structureherbelin
2003-06-20Ground Update.corbinea
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2002-12-19simplification de solve_subgoal: n'utilise plus frontierbarras
2002-12-09Option pour rendre les vérifications du refiner optionnelleherbelin
2002-05-29Réorganisation des tclTHEN (cf dev/changements.txt)herbelin
2001-11-12Suppression des stamps et donc des *_constraintsclrenard
2001-11-06Suite de la suppression : enamed_declaration est remplace par evar_map.clrenard
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-05-18Erreur dans un commentaire ...clrenard
2001-03-15entetesfilliatr
2001-02-01application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-12-02Portage d'AutoRewritedelahaye
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-13Code redondantherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-21Modifs d'interpretation de patternsdelahaye
2000-05-23Docherbelin
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
2000-05-04Nettoyage de l'interface de Pfeditherbelin
2000-05-03Ajout du langage de tactiquesdelahaye
1999-12-02modifs pour premiere edition de liensfilliatr
1999-12-01module Pfeditfilliatr
1999-10-20 - documentation repertoire proofs/filliatr
1999-10-19module Refinerfilliatr
1999-10-19les variables existentielles contiennent maintenant un environnement (typefilliatr
1999-10-18 - déplacement (encore une fois !) des variables existentielles : elles sontfilliatr