diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 17:15:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | 531590c223af42c07a93142ab0cea470a98964e6 (patch) | |
| tree | bfe531d8d32e491a66eceba60995702e20e73757 /proofs/clenv.ml | |
| parent | b36adb2124d3ba8a5547605e7f89bb0835d0ab10 (diff) | |
Removing compatibility layers in Retyping
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index a428ab0ed..393e958d3 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -62,7 +62,7 @@ let refresh_undefined_univs clenv = let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t -let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c) +let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause @@ -673,9 +673,7 @@ let evar_of_binder holes = function let define_with_type sigma env ev c = let open EConstr in let t = Retyping.get_type_of env sigma ev in - let t = EConstr.of_constr t in let ty = Retyping.get_type_of env sigma c in - let ty = EConstr.of_constr ty in let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in let (ev, _) = destEvar sigma ev in |