aboutsummaryrefslogtreecommitdiff
path: root/pretyping/clenv.mli
AgeCommit message (Expand)Author
2006-10-25Correction d'une tentative incorrecte (révision 9266) de clarificationherbelin
2006-10-24Ajout de la tactique "apply in".herbelin
2005-12-17Orthographe de 'instantiate'herbelin
2005-05-24Added clenv_environments_evars that behaves as clen_environments butsacerdot
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
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