diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/evd.mli | 45 | ||||
| -rw-r--r-- | engine/proofview.mli | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 26 | ||||
| -rw-r--r-- | engine/termops.mli | 3 | ||||
| -rw-r--r-- | engine/uState.ml | 2 | ||||
| -rw-r--r-- | engine/universes.ml | 2 |
7 files changed, 42 insertions, 40 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index a1cb0ec68e..8d465384b1 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -380,7 +380,7 @@ let add_name_newly_undefined id evk evi (evtoid, idtoev as names) = | None -> names | Some id -> if Id.Map.mem id idtoev then - user_err (str "Already an existential evar of name " ++ pr_id id); + user_err (str "Already an existential evar of name " ++ Id.print id); (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = diff --git a/engine/evd.mli b/engine/evd.mli index 45ca1a365a..af53735821 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -125,6 +125,7 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info (** {6 Unification state} **) type evar_universe_context = UState.t +[@@ocaml.deprecated "Alias of UState.t"] (** The universe context associated to an evar map *) type evar_map @@ -138,7 +139,7 @@ val from_env : env -> evar_map (** The empty evar map with given universe context, taking its initial universes from env. *) -val from_ctx : evar_universe_context -> evar_map +val from_ctx : UState.t -> evar_map (** The empty evar map with given universe context *) val is_empty : evar_map -> bool @@ -486,37 +487,37 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -type 'a in_evar_universe_context = 'a * evar_universe_context +type 'a in_evar_universe_context = 'a * UState.t -val evar_universe_context_set : evar_universe_context -> Univ.ContextSet.t -val evar_universe_context_constraints : evar_universe_context -> Univ.constraints -val evar_context_universe_context : evar_universe_context -> Univ.UContext.t -val evar_universe_context_of : Univ.ContextSet.t -> evar_universe_context -val empty_evar_universe_context : evar_universe_context -val union_evar_universe_context : evar_universe_context -> evar_universe_context -> - evar_universe_context -val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context +val evar_universe_context_set : UState.t -> Univ.ContextSet.t +val evar_universe_context_constraints : UState.t -> Univ.constraints +val evar_context_universe_context : UState.t -> Univ.UContext.t +val evar_universe_context_of : Univ.ContextSet.t -> UState.t +val empty_evar_universe_context : UState.t +val union_evar_universe_context : UState.t -> UState.t -> + UState.t +val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +val constrain_variables : Univ.LSet.t -> UState.t -> UState.t val evar_universe_context_of_binders : - Universes.universe_binders -> evar_universe_context + Universes.universe_binders -> UState.t -val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context +val make_evar_universe_context : env -> (Id.t located) 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 -> string -> Univ.Level.t val add_universe_name : evar_map -> string -> Univ.Level.t -> evar_map -val add_constraints_context : evar_universe_context -> - Univ.constraints -> evar_universe_context +val add_constraints_context : UState.t -> + Univ.constraints -> UState.t -val normalize_evar_universe_context_variables : evar_universe_context -> +val normalize_evar_universe_context_variables : UState.t -> Univ.universe_subst in_evar_universe_context -val normalize_evar_universe_context : evar_universe_context -> - evar_universe_context +val normalize_evar_universe_context : UState.t -> + UState.t val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -548,7 +549,7 @@ val set_eq_instances : ?flex:bool -> val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool -val evar_universe_context : evar_map -> evar_universe_context +val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> (Id.t * Univ.Level.t) list * Univ.UContext.t @@ -558,8 +559,8 @@ val universes : evar_map -> UGraph.t val check_univ_decl : evar_map -> UState.universe_decl -> Universes.universe_binders * Univ.UContext.t -val merge_universe_context : evar_map -> evar_universe_context -> evar_map -val set_universe_context : evar_map -> evar_universe_context -> evar_map +val merge_universe_context : evar_map -> UState.t -> evar_map +val set_universe_context : evar_map -> UState.t -> evar_map val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map @@ -567,7 +568,7 @@ val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst -val abstract_undefined_variables : evar_universe_context -> evar_universe_context +val abstract_undefined_variables : UState.t -> UState.t val fix_undefined_variables : evar_map -> evar_map diff --git a/engine/proofview.mli b/engine/proofview.mli index d92d0a7d53..0379d4b493 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -426,7 +426,7 @@ module Unsafe : sig val tclGETGOALS : Evd.evar list tactic (** Sets the evar universe context. *) - val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic + val tclEVARUNIVCONTEXT : UState.t -> unit tactic (** Clears the future goals store in the proof view. *) val reset_future_goals : proofview -> proofview diff --git a/engine/termops.ml b/engine/termops.ml index 78dbdb11aa..46fac50f22 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -50,13 +50,13 @@ let pr_puniverses p u = let rec pr_constr c = match kind c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" - | Var id -> pr_id id + | Var id -> Id.print id | Sort s -> print_sort s | Cast (c,_, t) -> hov 1 (str"(" ++ pr_constr c ++ cut() ++ str":" ++ pr_constr t ++ str")") | Prod (Name(id),t,c) -> hov 1 - (str"forall " ++ pr_id id ++ str":" ++ pr_constr t ++ str"," ++ + (str"forall " ++ Id.print id ++ str":" ++ pr_constr t ++ str"," ++ spc() ++ pr_constr c) | Prod (Anonymous,t,c) -> hov 0 (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ @@ -130,9 +130,9 @@ let pr_existential_key sigma evk = let open Evd in match evar_ident evk sigma with | None -> - str "?" ++ pr_id (pr_evar_suggested_name evk sigma) + str "?" ++ Id.print (pr_evar_suggested_name evk sigma) | Some id -> - str "?" ++ pr_id id + str "?" ++ Id.print id let pr_instance_status (sc,typ) = let open Evd in @@ -158,7 +158,7 @@ let pr_meta_map evd = let open Evd in let print_constr = print_kconstr in let pr_name = function - Name id -> str"[" ++ pr_id id ++ str"]" + Name id -> str"[" ++ Id.print id ++ str"]" | _ -> mt() in let pr_meta_binding = function | (mv,Cltyp (na,b)) -> @@ -178,23 +178,23 @@ let pr_decl (decl,ok) = let open NamedDecl in let print_constr = print_kconstr in match decl with - | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") - | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ + | LocalAssum (id,_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}") + | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++ print_constr c ++ str (if ok then ")" else "}") let pr_evar_source = function - | Evar_kinds.NamedHole id -> pr_id id + | Evar_kinds.NamedHole id -> Id.print id | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" | Evar_kinds.CasesType true -> str "subterm of pattern-matching return predicate" - | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id + | Evar_kinds.BinderType (Name id) -> str "type of " ++ Id.print id | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder" | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let open Globnames in let print_constr = print_kconstr in let id = Option.get ido in - str "parameter " ++ pr_id id ++ spc () ++ str "of" ++ + str "parameter " ++ Id.print id ++ spc () ++ str "of" ++ spc () ++ print_constr (printable_constr_of_global c) | Evar_kinds.InternalHole -> str "internal placeholder" | Evar_kinds.TomatchTypeParameter (ind,n) -> @@ -203,7 +203,7 @@ let pr_evar_source = function | Evar_kinds.GoalEvar -> str "goal evar" | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause" | Evar_kinds.MatchingVar _ -> str "matching variable" - | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id + | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id | Evar_kinds.SubEvar evk -> let open Evd in str "subterm of " ++ str (string_of_existential evk) @@ -435,7 +435,7 @@ let pr_var_decl env decl = (str" := " ++ pb ++ cut () ) in let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in let ptyp = (str" : " ++ pt) in - (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp)) + (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp)) let pr_rel_decl env decl = let open RelDecl in @@ -449,7 +449,7 @@ let pr_rel_decl env decl = let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in match get_name decl with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) - | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) let print_named_context env = hv 0 (fold_named_context diff --git a/engine/termops.mli b/engine/termops.mli index 2dab0685d6..793490798a 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -113,6 +113,7 @@ val collect_metas : Evd.evar_map -> constr -> int list val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *) +[@@ocaml.deprecated "alias of Termops.dependent"] (* Substitution of metavariables *) type meta_value_map = (metavariable * Constr.constr) list @@ -290,7 +291,7 @@ val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> evar_map -> Pp.t val pr_metaset : Metaset.t -> Pp.t -val pr_evar_universe_context : evar_universe_context -> Pp.t +val pr_evar_universe_context : UState.t -> Pp.t val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t (** debug printer: do not use to display terms to the casual user... *) diff --git a/engine/uState.ml b/engine/uState.ml index 77837fefcf..dfea25dd04 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -269,7 +269,7 @@ let universe_context ~names ~extensible ctx = try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) with Not_found -> user_err ?loc ~hdr:"universe_context" - (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + (str"Universe " ++ Id.print id ++ str" is not bound anymore.") in (l :: newinst, Univ.LSet.remove l acc)) names ([], levels) in diff --git a/engine/universes.ml b/engine/universes.ml index 3136f805c8..6c1b64d742 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -16,7 +16,7 @@ open Univ open Globnames let pr_with_global_universes l = - try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) + try Id.print (LMap.find l (snd (Global.global_universe_names ()))) with Not_found -> Level.pr l (** Local universe names of polymorphic references *) |