diff options
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index c238f731d..1ee6e0ca5 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -28,12 +28,12 @@ let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = - let t = NamedDecl.get_type decl in + let t = EConstr.of_constr (NamedDecl.get_type decl) in let evdref = ref sigma in let _ = Typing.e_sort_of env evdref t in let () = match decl with | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.e_check env evdref body t + | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t in (!evdref, Environ.push_named decl env) in @@ -42,7 +42,7 @@ let typecheck_evar ev env sigma = let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in + let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in !evdref let typecheck_proof c concl env sigma = @@ -101,6 +101,7 @@ let make_refine_enter ?(unsafe = true) f = else Pretype_errors.error_occur_check env sigma self c in (** Proceed to the refinement *) + let c = EConstr.Unsafe.to_constr c in let sigma = match evkmain with | None -> Evd.define self c sigma | Some evk -> |