From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 8 Nov 2016 19:02:40 +0100 Subject: Pretyping API using EConstr. --- interp/constrintern.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'interp/constrintern.ml') 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) -- cgit v1.2.3 From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- interp/constrintern.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8d4d87f2a2..e5dd6a6ec3 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) -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- interp/constrintern.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e5dd6a6ec3..41e2e4e6ff 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2083,6 +2083,7 @@ let intern_context global_level env impl_env binders = user_err ~loc ~hdr:"internalize" (explain_internalization_error e) let interp_rawcontext_evars env evdref k bl = + let open EConstr in let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> @@ -2093,7 +2094,6 @@ 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 @@ -2104,8 +2104,6 @@ let interp_rawcontext_evars env evdref k bl = (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 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) -- cgit v1.2.3 From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:41:31 +0100 Subject: Namegen primitives now apply on evar constrs. Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 41e2e4e6ff..bac97aa3f6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1843,7 +1843,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (add_name match_acc (loc,x)) ((loc,x)::var_acc) | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt -> let fresh = - Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in + Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in canonize_args t tt (fresh::forbidden_names) ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) | _ -> assert false in -- cgit v1.2.3