aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/clenv.ml
Commit message (Expand)AuthorAge
...
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* error if binder was already definedGravatar barras2004-09-23
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* simplification de clenvGravatar barras2004-09-10
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* deplacement de clenv vers pretypingGravatar barras2004-09-03