aboutsummaryrefslogtreecommitdiff
path: root/proofs/refiner.mli
AgeCommit message (Expand)Author
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 00:07:06 +0000