diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8d4d87f2a..e5dd6a6ec 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1982,7 +1982,7 @@ let interp_type env sigma ?(impls=empty_internalization_env) c = interp_gen IsType env sigma ~impls c let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ = - interp_gen (OfType (EConstr.of_constr typ)) env sigma ~impls c + interp_gen (OfType typ) env sigma ~impls c (* Not all evars expected to be resolved *) @@ -2001,7 +2001,7 @@ let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen_impls env evdref ~impls (OfType (EConstr.of_constr typ)) c + interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls IsType c @@ -2093,6 +2093,7 @@ let interp_rawcontext_evars env evdref k bl = let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> + let t = EConstr.Unsafe.to_constr t in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2102,7 +2103,9 @@ let interp_rawcontext_evars env evdref k bl = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_tcc_evars env evdref ~expected_type:(OfType (EConstr.of_constr t)) b in + let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in + let t = EConstr.Unsafe.to_constr t in + let c = EConstr.Unsafe.to_constr c in let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) |