aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/clenv.ml
Commit message (Expand)AuthorAge
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Added clenv_environments_evars that behaves as clen_environments butGravatar sacerdot2005-05-24
* 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