diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 3e3889cbb3..fd88e3c518 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -44,7 +44,7 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_nf_meta clenv c = nf_meta clenv.evd c +let clenv_nf_meta clenv c = EConstr.of_constr (nf_meta clenv.evd (EConstr.Unsafe.to_constr c)) let clenv_term clenv c = meta_instance clenv.evd c let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv let clenv_value clenv = meta_instance clenv.evd clenv.templval diff --git a/proofs/clenv.mli b/proofs/clenv.mli index e4f6f9a910..f7ff4bed34 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -36,7 +36,7 @@ val clenv_value : clausenv -> constr val clenv_type : clausenv -> types (** substitute resolved metas *) -val clenv_nf_meta : clausenv -> Constr.constr -> Constr.constr +val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types |