diff options
| author | Pierre-Marie Pédrot | 2016-11-08 19:02:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:27:26 +0100 |
| commit | 85ab3e298aa1d7333787c1fa44d25df189ac255c (patch) | |
| tree | 32f661f4ccd3fb36657bb9ac8104a08df9cd1d87 /interp | |
| parent | 67dc22d8389234d0c9b329944ff579e7056b7250 (diff) | |
Pretyping API using EConstr.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 235e6e24f6..8d4d87f2a2 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1937,7 +1937,7 @@ let extract_ids env = let scope_of_type_kind = function | IsType -> Notation.current_type_scope_name () - | OfType typ -> compute_type_scope typ + | OfType typ -> compute_type_scope (EConstr.Unsafe.to_constr typ) | WithoutTypeConstraint -> None let empty_ltac_sign = { @@ -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 typ) env sigma ~impls c + interp_gen (OfType (EConstr.of_constr 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 typ) c + interp_constr_evars_gen_impls env evdref ~impls (OfType (EConstr.of_constr typ)) c let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls IsType c @@ -2016,7 +2016,7 @@ let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen env evdref ~impls (OfType typ) c + interp_constr_evars_gen env evdref ~impls (OfType (EConstr.of_constr typ)) c let interp_type_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref IsType ~impls c @@ -2102,7 +2102,7 @@ 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 t) b in + let c = understand_tcc_evars env evdref ~expected_type:(OfType (EConstr.of_constr t)) b in let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) |