diff options
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2d621e97c..956be88c8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -669,12 +669,14 @@ let evar_of_binder holes = function user_err (str "No such binder.") let define_with_type sigma env ev c = + let c = EConstr.of_constr c in let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in - let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) 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 (EConstr.of_constr t) in let (ev, _) = destEvar ev in - let sigma = Evd.define ev j.Environ.uj_val sigma in + let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in sigma let solve_evar_clause env sigma hyp_only clause = function |