diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 6 | ||||
| -rw-r--r-- | engine/uState.mli | 2 | ||||
| -rw-r--r-- | engine/universes.ml | 4 | ||||
| -rw-r--r-- | engine/universes.mli | 2 |
6 files changed, 9 insertions, 9 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 0e9472158..2142cee37 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -802,7 +802,7 @@ let make_evar_universe_context e l = | None -> uctx | Some us -> List.fold_left - (fun uctx (loc,id) -> + (fun uctx { CAst.loc; v = id } -> fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx)) uctx us diff --git a/engine/evd.mli b/engine/evd.mli index b28ce2a62..84fa70ef2 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -506,7 +506,7 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t val evar_universe_context_of_binders : Universes.universe_binders -> UState.t -val make_evar_universe_context : env -> (Id.t located) list option -> UState.t +val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t diff --git a/engine/uState.ml b/engine/uState.ml index 4b650c9c9..625495866 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -282,7 +282,7 @@ let pr_uctx_level uctx l = Libnames.pr_reference (reference_of_level uctx l) type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl let error_unbound_universes left uctx = let open Univ in @@ -305,7 +305,7 @@ let universe_context ~names ~extensible uctx = let levels = ContextSet.levels uctx.uctx_local in let newinst, left = List.fold_right - (fun (loc,id) (newinst, acc) -> + (fun { CAst.loc; v = id } (newinst, acc) -> let l = try UNameMap.find id (fst uctx.uctx_names) with Not_found -> assert false @@ -325,7 +325,7 @@ let check_universe_context_set ~names ~extensible uctx = if extensible then () else let open Univ in - let left = List.fold_left (fun left (loc,id) -> + let left = List.fold_left (fun left { CAst.loc; v = id } -> let l = try UNameMap.find id (fst uctx.uctx_names) with Not_found -> assert false diff --git a/engine/uState.mli b/engine/uState.mli index 6657d6047..5c85b2b84 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -132,7 +132,7 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl (** [check_univ_decl ctx decl] diff --git a/engine/universes.ml b/engine/universes.ml index 3a00f0fd1..f3660a559 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -92,14 +92,14 @@ let register_universe_binders ref ubinders = if not (Id.Map.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) -type univ_name_list = Name.t Loc.located list +type univ_name_list = Misctypes.lname list let universe_binders_with_opt_names ref levels = function | None -> universe_binders_of_global ref | Some udecl -> if Int.equal(List.length levels) (List.length udecl) then - List.fold_left2 (fun acc (_,na) lvl -> match na with + List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with | Anonymous -> acc | Name na -> Names.Id.Map.add na lvl acc) empty_binders udecl levels diff --git a/engine/universes.mli b/engine/universes.mli index cb6e2ba1b..04586a6f8 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -35,7 +35,7 @@ val empty_binders : universe_binders val register_universe_binders : Globnames.global_reference -> universe_binders -> unit val universe_binders_of_global : Globnames.global_reference -> universe_binders -type univ_name_list = Name.t Loc.located list +type univ_name_list = Misctypes.lname list (** [universe_binders_with_opt_names ref u l] |