diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 8 | ||||
| -rw-r--r-- | interp/declare.mli | 2 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 2 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 4 | ||||
| -rw-r--r-- | interp/impargs.ml | 10 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 2 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 32 | ||||
| -rw-r--r-- | interp/reserve.ml | 4 |
10 files changed, 36 insertions, 32 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index c55a6c69ba..bc2d2068a2 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -487,7 +487,7 @@ let add_universe src (dp, i) = Option.iter (fun poly -> let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in Global.push_context_set poly ctx; - Universes.add_global_universe level poly; + UnivNames.add_global_universe level poly; if poly then Lib.add_section_context ctx) optpoly @@ -538,7 +538,7 @@ let input_universe : universe_decl -> Libobject.obj = let declare_univ_binders gr pl = if Global.is_polymorphic gr then - Universes.register_universe_binders gr pl + UnivNames.register_universe_binders gr pl else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c @@ -564,7 +564,7 @@ let do_universe poly l = in let l = List.map (fun {CAst.v=id} -> - let lev = Universes.new_univ_id () in + let lev = UnivGen.new_univ_id () in (id, lev)) l in let src = if poly then BoundUniv else UnqualifiedUniv in @@ -595,7 +595,7 @@ let input_constraints : constraint_decl -> Libobject.obj = let do_constraint poly l = let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - Universes.is_polymorphic level, level + UnivNames.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = diff --git a/interp/declare.mli b/interp/declare.mli index de4d8346a4..4a9f542783 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -83,7 +83,7 @@ val recursive_message : bool (** true = fixpoint *) -> val exists_name : Id.t -> bool (** Global universe contexts, names and constraints *) -val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit +val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index bc6a1ef3aa..74618a2905 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc -> let dump_definition {CAst.loc;v=id} sec s = dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) -let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty = +let dump_constraint { CAst.loc; v = n } sec ty = match n with | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty | Names.Anonymous -> () diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 8dfb4f8f7f..bf83d2df40 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -38,8 +38,8 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit val dump_notation : (Constrexpr.notation * Notation.notation_location) Loc.located -> Notation_term.scope_name option -> bool -> unit -val dump_constraint : - Vernacexpr.typeclass_constraint -> bool -> string -> unit + +val dump_constraint : Misctypes.lname -> bool -> string -> unit val dump_string : string -> unit diff --git a/interp/impargs.ml b/interp/impargs.ml index 7e4c4ef4f7..8aa1e62504 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -237,11 +237,11 @@ let is_rigid env sigma t = is_rigid_head sigma t | _ -> true -let find_displayed_name_in all avoid na (env, b) = +let find_displayed_name_in sigma all avoid na (env, b) = let envnames_b = (env, b) in let flag = RenamingElsewhereFor envnames_b in - if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b - else compute_displayed_name_in Evd.empty flag avoid na b + if all then compute_and_force_displayed_name_in sigma flag avoid na b + else compute_displayed_name_in sigma flag avoid na b let compute_implicits_names_gen all env sigma t = let open Context.Rel.Declaration in @@ -249,7 +249,7 @@ let compute_implicits_names_gen all env sigma t = let t = whd_all env sigma t in match kind sigma t with | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in all avoid na (names,b) in + let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b | _ -> List.rev names in aux env Id.Set.empty [] t @@ -538,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (subst,(req,l)) = - (ImplLocal,List.smartmap (subst_implicits_decl subst) l) + (ImplLocal,List.Smart.map (subst_implicits_decl subst) l) let impls_of_context ctx = let map (decl, impl) = match impl with diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 58df9abc4a..289890544f 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -58,7 +58,7 @@ let in_generalizable : bool * Misctypes.lident list option -> obj = classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj) } -let declare_generalizable local gen = +let declare_generalizable ~local gen = Lib.add_anonymous_leaf (in_generalizable (local, gen)) let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 5f4129ae0c..39d0174f99 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -13,7 +13,7 @@ open Glob_term open Constrexpr open Libnames -val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit +val declare_generalizable : local:bool -> Misctypes.lident list option -> unit val ids_of_list : Id.t list -> Id.Set.t val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t diff --git a/interp/notation.ml b/interp/notation.ml index e6df7b96c9..192c477be7 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -741,7 +741,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) = match subst_scope_class subst cl with | Some cl' as ocl' when cl' != cl -> ocl' | _ -> ocl in - let cls' = List.smartmap subst_cl cls in + let cls' = List.Smart.map subst_cl cls in (ArgsScopeNoDischarge,r',n,scl,cls') let discharge_arguments_scope (_,(req,r,n,l,_)) = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index b806dce0b1..448881dcf9 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -509,7 +509,9 @@ let notation_constr_of_glob_constr nenv a = let notation_constr_of_constr avoiding t = let t = EConstr.of_constr t in - let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in + let env = Global.env () in + let evd = Evd.from_env env in + let t = Detyping.detype Detyping.Now false avoiding env evd t in let nenv = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; @@ -521,7 +523,7 @@ let rec subst_pat subst pat = | PatVar _ -> pat | PatCstr (((kn,i),j),cpl,n) -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_pat subst) cpl in + and cpl' = List.Smart.map (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n) @@ -536,7 +538,7 @@ let rec subst_notation_constr subst bound raw = | NApp (r,rl) -> let r' = subst_notation_constr subst bound r - and rl' = List.smartmap (subst_notation_constr subst bound) rl in + and rl' = List.Smart.map (subst_notation_constr subst bound) rl in if r' == r && rl' == rl then raw else NApp(r',rl') @@ -566,14 +568,14 @@ let rec subst_notation_constr subst bound raw = | NLetIn (n,r1,t,r2) -> let r1' = subst_notation_constr subst bound r1 in - let t' = Option.smartmap (subst_notation_constr subst bound) t in + let t' = Option.Smart.map (subst_notation_constr subst bound) t in let r2' = subst_notation_constr subst bound r2 in if r1' == r1 && t == t' && r2' == r2 then raw else NLetIn (n,r1',t',r2') | NCases (sty,rtntypopt,rl,branches) -> - let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt - and rl' = List.smartmap + let rtntypopt' = Option.Smart.map (subst_notation_constr subst bound) rtntypopt + and rl' = List.Smart.map (fun (a,(n,signopt) as x) -> let a' = subst_notation_constr subst bound a in let signopt' = Option.map (fun ((indkn,i),nal as z) -> @@ -581,9 +583,9 @@ let rec subst_notation_constr subst bound raw = if indkn == indkn' then z else ((indkn',i),nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun (cpl,r as branch) -> - let cpl' = List.smartmap (subst_pat subst) cpl + let cpl' = List.Smart.map (subst_pat subst) cpl and r' = subst_notation_constr subst bound r in if cpl' == cpl && r' == r then branch else (cpl',r')) @@ -594,14 +596,14 @@ let rec subst_notation_constr subst bound raw = NCases (sty,rtntypopt',rl',branches') | NLetTuple (nal,(na,po),b,c) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b' = subst_notation_constr subst bound b and c' = subst_notation_constr subst bound c in if po' == po && b' == b && c' == c then raw else NLetTuple (nal,(na,po'),b',c') | NIf (c,(na,po),b1,b2) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b1' = subst_notation_constr subst bound b1 and b2' = subst_notation_constr subst bound b2 and c' = subst_notation_constr subst bound c in @@ -610,12 +612,12 @@ let rec subst_notation_constr subst bound raw = | NRec (fk,idl,dll,tl,bl) -> let dll' = - Array.smartmap (List.smartmap (fun (na,oc,b as x) -> - let oc' = Option.smartmap (subst_notation_constr subst bound) oc in + Array.Smart.map (List.Smart.map (fun (na,oc,b as x) -> + let oc' = Option.Smart.map (subst_notation_constr subst bound) oc in let b' = subst_notation_constr subst bound b in if oc' == oc && b' == b then x else (na,oc',b'))) dll in - let tl' = Array.smartmap (subst_notation_constr subst bound) tl in - let bl' = Array.smartmap (subst_notation_constr subst bound) bl in + let tl' = Array.Smart.map (subst_notation_constr subst bound) tl in + let bl' = Array.Smart.map (subst_notation_constr subst bound) bl in if dll' == dll && tl' == tl && bl' == bl then raw else NRec (fk,idl,dll',tl',bl') @@ -628,7 +630,7 @@ let rec subst_notation_constr subst bound raw = if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in + let nsolve = Option.Smart.map (Genintern.generic_substitute subst) solve in if nsolve == solve && nknd == knd then raw else NHole (nknd, naming, nsolve) diff --git a/interp/reserve.ml b/interp/reserve.ml index b57103cf22..071248f01f 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -112,7 +112,9 @@ let revert_reserved_type t = let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in let t = EConstr.of_constr t in - let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in + let env = Global.env () in + let evd = Evd.from_env env in + let t = Detyping.detype Detyping.Now false Id.Set.empty env evd t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = |