diff options
| author | herbelin | 2007-05-23 10:29:01 +0000 |
|---|---|---|
| committer | herbelin | 2007-05-23 10:29:01 +0000 |
| commit | b483e1732682bd1b8cec8d5d3a600c93d90f44ab (patch) | |
| tree | 73061a8da273c859530bbf90b61e8f9ad01ccb34 /pretyping/evd.mli | |
| parent | 500aaf4e5ab37550efc0e0493b0afa45eaf250d3 (diff) | |
Suite restructuration unification et division des problèmes
d'unification des types des with-bindings en deux: les problèmes
d'unification susceptibles d'introduire une coercion sont retardés
(comme dans le commit r9850) et ceux susceptibles de fournir d'autres
instances restent faits au plus tôt (comme avant le commit r9850).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9851 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 784e066b71..b6ffd02c12 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -112,7 +112,8 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted *) type instance_status = - IsSuperType | IsSubType | ConvUpToEta of int | Coercible of types + | IsSuperType | IsSubType + | ConvUpToEta of int | Coercible of types | Processed type clbinding = | Cltyp of name * constr freelisted @@ -180,7 +181,7 @@ val metas_of : evar_defs -> metamap type metabinding = metavariable * constr * instance_status -val retract_defined_metas : evar_defs -> metabinding list * evar_defs +val retract_coercible_metas : evar_defs -> metabinding list * evar_defs val subst_defined_metas : metabinding list -> constr -> constr option (**********************************************************) |