aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.mli
Commit message (Expand)AuthorAge
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 23:44:16 +0000