diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 73 |
1 files changed, 5 insertions, 68 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b4d87dfdb0..40b8bcad92 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -47,8 +47,6 @@ open Misctypes module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * EConstr.constr (************************************************************************) (* This concerns Cases *) @@ -385,9 +383,6 @@ let adjust_evar_source evdref na c = end | _, _ -> c -(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) -let allow_anonymous_refs = ref false - (* coerce to tycon if any *) let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function | None -> j @@ -918,9 +913,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* Make dependencies from arity signature impossible *) let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in - if not !allow_anonymous_refs then - List.map (set_name Anonymous) arsgn - else arsgn + List.map (set_name Anonymous) arsgn in let indt = build_dependent_inductive env.ExtraEnv.env indf in let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) @@ -981,10 +974,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in - if not !allow_anonymous_refs then - (* Make dependencies from arity signature impossible *) - List.map (set_name Anonymous) arsgn - else arsgn + (* Make dependencies from arity signature impossible *) + List.map (set_name Anonymous) arsgn in let nar = List.length arsgn in let indt = build_dependent_inductive env.ExtraEnv.env indf in @@ -1018,13 +1009,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in let csgn = - if not !allow_anonymous_refs then - List.map (set_name Anonymous) cs_args - else - List.map (map_name (function Name _ as n -> n - | Anonymous -> Name Namegen.default_non_dependent_ident)) - cs_args - in + List.map (set_name Anonymous) cs_args + in let env_c = push_rel_context !evdref csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs_args in @@ -1191,29 +1177,6 @@ let no_classes_no_fail_inference_flags = { let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false -let on_judgment sigma f j = - let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in - let (c,_,t) = destCast sigma (f c) in - {uj_val = c; uj_type = t} - -let understand_judgment env sigma c = - let env = make_env env sigma in - let evdref = ref sigma in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - let j = on_judgment sigma (fun c -> - let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in - evdref := evd; c) j - in j, Evd.evar_universe_context !evdref - -let understand_judgment_tcc env evdref c = - let env = make_env env !evdref in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - on_judgment !evdref (fun c -> - let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in - evdref := evd; c) j - let ise_pretype_gen_ctx flags env sigma lvar kind c = let evd, c = ise_pretype_gen flags env sigma lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in @@ -1231,36 +1194,10 @@ let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutT let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in (sigma, c) -let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c = - let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in - evdref := sigma; - c - let understand_ltac flags env sigma lvar kind c = let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let constr_flags = { - use_typeclasses = true; - solve_unification_constraints = true; - use_hook = None; - fail_evar = true; - expand_evars = true } - -(* Fully evaluate an untyped constr *) -let type_uconstr ?(flags = constr_flags) - ?(expected_type = WithoutTypeConstraint) ist c = - begin fun env sigma -> - let { closure; term } = c in - let vars = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = Id.Map.empty; - } in - understand_ltac flags env sigma vars expected_type term - end - let pretype k0 resolve_tc typcon env evdref lvar t = pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t |