aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.mli
Commit message (Expand)AuthorAge
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* - coqmktopGravatar filliatr1999-12-03
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* module WcclausenvGravatar filliatr1999-11-22
* module Clenv (debut)Gravatar filliatr1999-10-20