aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenv.ml
AgeCommit message (Expand)Author
2000-05-18bug (typage avec meta)herbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-04-28chgt unify_0herbelin
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
2000-03-21Remplacement plain_instance en instance qui n'a plus besoin de envherbelin
2000-03-17Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'herbelin
1999-12-14rattrapage exceptions autres que UserErrorfilliatr
1999-12-14bug mk_clenv_from lorsque pas d argumentsfilliatr
1999-12-13 - états fabriqués avec -silentfilliatr
1999-12-05premier debugagefilliatr
1999-12-03 - coqmktopfilliatr
1999-12-02modifs pour premiere edition de liensfilliatr
1999-12-01 - Typing -> Safe_typingfilliatr
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
1999-11-22module Wcclausenvfilliatr
1999-10-20 - documentation repertoire proofs/filliatr
1999-10-20module Clenv (debut)filliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 23:12:55 +0000