Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.

10 files changed, 39 insertions, 36 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5ef7fac814..16798a1d57 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -154,7 +154,7 @@ let error_incompatible_inst clenv mv  =
       Name id ->
         user_err ~hdr:"clenv_assign"
           (str "An incompatible instantiation has already been found for " ++
-           pr_id id)
+           Id.print id)
     | _ ->
         anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.")
 
@@ -417,7 +417,7 @@ let check_bindings bl =
   match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with
     | NamedHyp s :: _ ->
 	user_err 
-	  (str "The variable " ++ pr_id s ++
+	  (str "The variable " ++ Id.print s ++
 	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
 	user_err 
@@ -435,12 +435,12 @@ let explain_no_such_bound_variable evd id =
   in
   let mvl = List.fold_left fold [] (Evd.meta_list evd) in
   user_err ~hdr:"Evd.meta_with_name"
-    (str"No such bound variable " ++ pr_id id ++
+    (str"No such bound variable " ++ Id.print id ++
      (if mvl == [] then str " (no bound variables at all in the expression)."
       else
         (str" (possible name" ++
          str (if List.length mvl == 1 then " is: " else "s are: ") ++
-         pr_enum pr_id mvl ++ str").")))
+         pr_enum Id.print mvl ++ str").")))
 
 let meta_with_name evd id =
   let na = Name id in
@@ -460,7 +460,7 @@ let meta_with_name evd id =
         n
     | _  ->
         user_err ~hdr:"Evd.meta_with_name"
-          (str "Binder name \"" ++ pr_id id ++
+          (str "Binder name \"" ++ Id.print id ++
            strbrk "\" occurs more than once in clause.")
 
 let meta_of_binder clause loc mvs = function
@@ -474,7 +474,7 @@ let error_already_defined b =
   match b with
     | NamedHyp id ->
         user_err 
-          (str "Binder name \"" ++ pr_id id ++
+          (str "Binder name \"" ++ Id.print id ++
            str"\" already defined with incompatible value.")
     | AnonHyp n ->
         anomaly
@@ -639,10 +639,10 @@ let explain_no_such_bound_variable holes id =
   let mvl = List.fold_right fold holes [] in
   let expl = match mvl with
   | [] -> str " (no bound variables at all in the expression)."
-  | [id] -> str "(possible name is: " ++ pr_id id ++ str ")."
-  | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")."
+  | [id] -> str "(possible name is: " ++ Id.print id ++ str ")."
+  | _ -> str "(possible names are: " ++ pr_enum Id.print mvl ++ str ")."
   in
-  user_err  (str "No such bound variable " ++ pr_id id ++ expl)
+  user_err  (str "No such bound variable " ++ Id.print id ++ expl)
 
 let evar_with_name holes id =
   let map h = match h.hole_name with
@@ -655,7 +655,7 @@ let evar_with_name holes id =
   | [h] -> h.hole_evar
   | _ ->
     user_err 
-      (str "Binder name \"" ++ pr_id id ++
+      (str "Binder name \"" ++ Id.print id ++
         str "\" occurs more than once in clause.")
 
 let evar_of_binder holes = function
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a633238f43..13a4e4ce31 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -140,9 +140,9 @@ let reorder_context env sigma sign ord =
           let ((d,h),mh) = find_q top moved_hyps in
           if occur_vars_in_decl env sigma h d then
             user_err ~hdr:"reorder_context"
-              (str "Cannot move declaration " ++ pr_id top ++ spc() ++
+              (str "Cannot move declaration " ++ Id.print top ++ spc() ++
               str "before " ++
-              pr_sequence pr_id
+              pr_sequence Id.print
                 (Id.Set.elements (Id.Set.inter h
                   (global_vars_set_of_decl env sigma d))));
           step ord' expected ctxt_head mh (d::ctxt_tail)
@@ -173,7 +173,7 @@ let check_decl_position env sigma sign d =
   let deps = dependency_closure env sigma (named_context_of_val sign) needed in
   if Id.List.mem x deps then
     user_err ~hdr:"Logic.check_decl_position"
-      (str "Cannot create self-referring hypothesis " ++ pr_id x);
+      (str "Cannot create self-referring hypothesis " ++ Id.print x);
   x::deps
 
 (* Auxiliary functions for primitive MOVE tactic
@@ -234,10 +234,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
-	        Miscprint.pr_move_location pr_id hto ++
+	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
+	        Miscprint.pr_move_location Id.print hto ++
 	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
-	        ++ pr_id hyp ++ str ".")
+	        ++ Id.print hyp ++ str ".")
           else
 	    (d::first, middle)
 	in
@@ -507,10 +507,10 @@ let convert_hyp check sign sigma d =
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then
 	  user_err ~hdr:"Logic.convert_hyp"
-            (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
+            (str "Incorrect change of the type of " ++ Id.print id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
 	  user_err ~hdr:"Logic.convert_hyp"
-            (str "Incorrect change of the body of "++ pr_id id ++ str ".");
+            (str "Incorrect change of the body of "++ Id.print id ++ str ".");
        if check then reorder := check_decl_position env sigma sign d;
        map_named_decl EConstr.Unsafe.to_constr d) in
   reorder_val_context env sigma sign' !reorder
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index 5d37c8a024..92b58b4092 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -6,8 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Misctypes
 open Pp
+open Names
+open Misctypes
 
 (** Printing of [intro_pattern] *)
 
@@ -18,8 +19,8 @@ let rec pr_intro_pattern prc (_,pat) = match pat with
   | IntroAction p -> pr_intro_pattern_action prc p
 
 and pr_intro_pattern_naming = function
-  | IntroIdentifier id -> Nameops.pr_id id
-  | IntroFresh id -> str "?" ++ Nameops.pr_id id
+  | IntroIdentifier id -> Id.print id
+  | IntroFresh id -> str "?" ++ Id.print id
   | IntroAnonymous -> str "?"
 
 and pr_intro_pattern_action prc = function
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 21a65f8eb6..d676a0874b 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -95,14 +95,14 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
     tactic. *)
 
 val build_constant_by_tactic :
-  Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
+  Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
   EConstr.types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool *
-    Evd.evar_universe_context
+    UState.t
 
-val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
+val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
   EConstr.types -> unit Proofview.tactic -> 
-  constr * bool * Evd.evar_universe_context
+  constr * bool * UState.t
 
 val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
   constr * Evd.evar_map
diff --git a/proofs/proof.ml b/proofs/proof.ml
index ba4980b66b..e24d57f088 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -112,7 +112,7 @@ type proof = {
   (* List of goals that have been given up *)
   given_up : Goal.goal list;
   (* The initial universe context (for the statement) *)
-  initial_euctx : Evd.evar_universe_context
+  initial_euctx : UState.t
 }
 
 (*** General proof functions ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 698aa48b02..48aed8225e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -69,7 +69,7 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
 val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
 val dependent_start : Proofview.telescope -> proof
 val initial_goals : proof -> (EConstr.constr * EConstr.types) list
-val initial_euctx : proof -> Evd.evar_universe_context
+val initial_euctx : proof -> UState.t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 97faa16848..fdc9a236bf 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,7 +68,7 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type proof_universes = UState.t * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
@@ -185,7 +185,7 @@ let msg_proofs () =
   match get_all_proof_names () with
     | [] -> (spc () ++ str"(No proof-editing in progress).")
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (pr_sequence Nameops.pr_id l) ++ str".")
+               (pr_sequence Id.print l) ++ str".")
 
 let there_is_a_proof () = not (List.is_empty !pstates)
 let there_are_pending_proofs () = there_is_a_proof ()
@@ -320,7 +320,7 @@ let constrain_variables init uctx =
   let levels = Univ.Instance.levels (Univ.UContext.instance init) in
   UState.constrain_variables levels uctx
 
-type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6309f681f8..eed62f912e 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -33,7 +33,7 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type proof_universes = UState.t * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
@@ -86,7 +86,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 9c8777c413..34e517aedc 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -35,10 +35,10 @@ val tclIDTAC_MESSAGE  : Pp.t -> tactic
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
-val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+val tclEVARUNIVCONTEXT : UState.t -> tactic
 
 val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic
-val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
 
 val tclPUSHCONSTRAINTS : Univ.constraints -> tactic
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 6441cfd195..d9496d2b4f 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -10,7 +10,6 @@ open Names
 open Constr
 open Environ
 open EConstr
-open Evd
 open Proof_type
 open Redexpr
 open Pattern
@@ -19,7 +18,10 @@ open Ltac_pretype
 
 (** Operations for handling terms under a local typing context. *)
 
-type 'a sigma   = 'a Evd.sigma;;
+type 'a sigma   = 'a Evd.sigma
+[@@ocaml.deprecated "alias of Evd.sigma"]
+
+open Evd
 type tactic     = Proof_type.tactic;;
 
 val sig_it  : 'a sigma   -> 'a