diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 52 |
1 files changed, 39 insertions, 13 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 02c3c047d5..c7ed066f7e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -534,15 +534,19 @@ let intern_generalized_binder intern_type ntnvars in let na = match na with | Anonymous -> - let name = - let id = - match ty with - | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> - qualid_basename qid - | _ -> default_non_dependent_ident - in Implicit_quantifiers.make_fresh ids' (Global.env ()) id - in Name name - | _ -> na in + let id = + match ty with + | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> + qualid_basename qid + | _ -> default_non_dependent_ident + in + let ids' = List.fold_left (fun ids' lid -> Id.Set.add lid.CAst.v ids') ids' fvs in + let id = + Implicit_quantifiers.make_fresh ids' (Global.env ()) id + in + Name id + | _ -> na + in let impls = impls_type_list 1 ty' in (push_name_env ntnvars impls env' (make ?loc na), (make ?loc (na,b',ty')) :: List.rev bl) @@ -2409,8 +2413,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = and intern_args env subscopes = function | [] -> [] | a::args -> - let (enva,subscopes) = apply_scope_env env subscopes in - (intern_no_implicit enva a) :: (intern_args env subscopes args) + let (enva,subscopes) = apply_scope_env env subscopes in + let a = intern_no_implicit enva a in + a :: (intern_args env subscopes args) in intern env c @@ -2648,13 +2653,34 @@ let interp_univ_decl env decl = let binders : lident list = decl.univdecl_instance in let evd = Evd.from_env ~binders env in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in - let decl = { univdecl_instance = binders; + let decl = { + univdecl_instance = binders; univdecl_extensible_instance = decl.univdecl_extensible_instance; univdecl_constraints = cstrs; - univdecl_extensible_constraints = decl.univdecl_extensible_constraints } + univdecl_extensible_constraints = decl.univdecl_extensible_constraints; + } in evd, decl +let interp_cumul_univ_decl env decl = + let open UState in + let binders = List.map fst decl.univdecl_instance in + let variances = Array.map_of_list snd decl.univdecl_instance in + let evd = Evd.from_ctx (UState.from_env ~binders env) in + let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in + let decl = { + univdecl_instance = binders; + univdecl_extensible_instance = decl.univdecl_extensible_instance; + univdecl_constraints = cstrs; + univdecl_extensible_constraints = decl.univdecl_extensible_constraints; + } + in + evd, decl, variances + let interp_univ_decl_opt env l = match l with | None -> Evd.from_env env, UState.default_univ_decl | Some decl -> interp_univ_decl env decl + +let interp_cumul_univ_decl_opt env = function + | None -> Evd.from_env env, UState.default_univ_decl, [| |] + | Some decl -> interp_cumul_univ_decl env decl |