diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 41 |
1 files changed, 11 insertions, 30 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 521fa2247..4f9fbddda 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,7 +28,6 @@ open Names open Evd open Term open Vars -open Context open Termops open Reductionops open Environ @@ -47,7 +46,7 @@ open Misctypes type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t +type unbound_ltac_var_map = Genarg.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; ltac_uconstrs : uconstr_var_map; @@ -95,10 +94,6 @@ let search_guard loc env possible_indexes fixdefs = user_err_loc (loc,"search_guard", Pp.str errmsg) with Found indexes -> indexes) -(* To embed constr in glob_constr *) -let ((constr_in : constr -> Dyn.t), - (constr_out : Dyn.t -> constr)) = Dyn.create "constr" - (* To force universe name declaration before use *) let strict_universe_declarations = ref true @@ -134,7 +129,7 @@ let interp_universe_level_name evd (loc,s) = let level = Univ.Level.make dp num in let evd = try Evd.add_global_univ evd level - with Univ.AlreadyDeclared -> evd + with UGraph.AlreadyDeclared -> evd in evd, level else try @@ -321,7 +316,7 @@ let ltac_interp_name_env k0 lvar env = specification of pretype which accepts to start with a non empty rel_context) *) (* tail is the part of the env enriched by pretyping *) - let n = rel_context_length (rel_context env) - k0 in + let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in let env = pop_rel_context n env in let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in @@ -454,26 +449,12 @@ let new_type_evar env evdref loc = univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref in e -let get_projection env cst = - let cb = lookup_constant cst env in - match cb.Declarations.const_proj with - | Some {Declarations.proj_ind = mind; proj_npars = n; - proj_arg = m; proj_type = ty} -> - (cst,mind,n,m,ty) - | None -> raise Not_found - let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) -let is_GHole = function - | GHole _ -> true - | _ -> false - -let evars = ref Id.Map.empty - let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type k0 resolve_tc in @@ -539,14 +520,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let ty' = pretype_type empty_valcon env evdref lvar ty in let dcl = (na,None,ty'.utj_val) in let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl + type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in let dcl = (na,Some bd'.uj_val,ty'.utj_val) in let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in - let ctxtv = Array.map (type_bl env empty_rel_context) bl in + type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in + let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = Array.map2 (fun e ar -> @@ -573,7 +554,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) let (ctxt,ty) = - decompose_prod_n_assum (rel_context_length ctxt) + decompose_prod_n_assum (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in let nenv = push_rel_context ctxt newenv in let j = pretype (mk_tycon ty) nenv evdref lvar def in @@ -894,7 +875,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let pred = nf_evar !evdref pred in let p = nf_evar !evdref p in let f cs b = - let n = rel_context_length cs.cs_args in + let n = Context.Rel.length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist (pi, [build_dependent_constructor cs]) in let csgn = @@ -1027,7 +1008,7 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function let ise_pretype_gen flags env sigma lvar kind c = let evdref = ref sigma in - let k0 = rel_context_length (rel_context env) in + let k0 = Context.Rel.length (rel_context env) in let c' = match kind with | WithoutTypeConstraint -> (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val @@ -1069,7 +1050,7 @@ let on_judgment f j = let understand_judgment env sigma c = let evdref = ref sigma in - let k0 = rel_context_length (rel_context env) 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 (fun c -> let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in @@ -1077,7 +1058,7 @@ let understand_judgment env sigma c = in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = - let k0 = rel_context_length (rel_context env) 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 (fun c -> let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in |