aboutsummaryrefslogtreecommitdiff
path: root/pretyping/clenv.ml
AgeCommit message (Expand)Author
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-04-07- Documentation of the Program tactics.msozeau
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-05-24Added clenv_environments_evars that behaves as clen_environments butsacerdot
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-09-23error if binder was already definedbarras
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-10simplification de clenvbarras
2004-09-08unification encore...barras
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-03deplacement de clenv vers pretypingbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 04:39:07 +0000