Cleanup: removal of constr_of_global.

Constrintern.pf_global returns a global_reference, not a constr,
adapt plugins accordingly, properly registering universes where
necessary.

9 files changed, 67 insertions, 57 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7fad65bf0..92e3e8c9e 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -113,13 +113,17 @@ In Coqlib / reference location:
   We have removed from Coqlib functions returning `constr` from
   names. Now it is only possible to obtain references, that must be
   processed wrt the particular needs of the client.
+  We have changed in constrintern the functions returnin `constr` as
+  well to return global references instead.
 
   Users of `coq_constant/gen_constant` can do
   `Universes.constr_of_global (find_reference dir r)` _however_ note
   the warnings in the `Universes.constr_of_global` in the
   documentation. It is very likely that you were previously suffering
   from problems with polymorphic universes due to using
-  `Coqlib.coq_constant` that used to do this.
+  `Coqlib.coq_constant` that used to do this. You must rather use
+  `pf_constr_of_global` in tactics and `Evarutil.new_global` variants
+  when constructing terms in ML (see univpoly.txt for more information).
 
 ** Tactic API **
 
@@ -127,6 +131,10 @@ In Coqlib / reference location:
   Thus it only generates one instance of the global reference, and it is the
   caller's responsibility to perform a focus on the goal.
 
+- pf_global, construct_reference, global_reference,
+  global_reference_in_absolute_module now return a global_reference
+  instead of a constr.
+
 - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
   was very specific. Use tclPROGRESS instead.
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287ef..628c85e75 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -98,16 +98,16 @@ let global_reference_of_reference ref =
   locate_reference (snd (qualid_of_reference ref))
 
 let global_reference id =
-  Universes.constr_of_global (locate_reference (qualid_of_ident id))
+  locate_reference (qualid_of_ident id)
 
 let construct_reference ctx id =
   try
-    Term.mkVar (let _ = Context.Named.lookup id ctx in id)
+    VarRef (let _ = Context.Named.lookup id ctx in id)
   with Not_found ->
     global_reference id
 
 let global_reference_in_absolute_module dir id =
-  Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
+  Nametab.global_of_path (Libnames.make_path dir id)
 
 (**********************************************************************)
 (* Internalization errors                                             *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 644cafe57..644f60d85 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -176,9 +176,9 @@ val interp_context_evars :
 
 val locate_reference :  Libnames.qualid -> Globnames.global_reference
 val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr
-val global_reference : Id.t -> constr
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference
+val global_reference : Id.t -> Globnames.global_reference
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference
 
 (** Interprets a term as the left-hand side of a notation. The returned map is
     guaranteed to have the same domain as the input one. *)
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b2c8489ce..763443717 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -133,20 +133,6 @@ let prNamedRLDecl s lc =
     prstr "\n";
   end
 
-let showind (id:Id.t) =
-  let cstrid = Constrintern.global_reference id in
-  let (ind1, u),cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
-  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
-  let u = EConstr.Unsafe.to_instance u in
-  List.iter (fun decl ->
-    print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
-    prconstr (RelDecl.get_type decl); print_string "\n")
-    ib1.mind_arity_ctxt;
-    Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) (ind1, u));
-  Array.iteri
-    (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
-    ib1.mind_user_lc
-
 (** {2 Misc} *)
 
 exception Found of int
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ee748567b..d7408e88e 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -39,10 +39,10 @@ open OmegaSolver
 
 let elim_id id =
   Proofview.Goal.enter { enter = begin fun gl ->
-    simplest_elim (Tacmach.New.pf_global id gl)
+    simplest_elim (mkVar id)
   end }
 let resolve_id id = Proofview.Goal.enter { enter = begin fun gl ->
-  apply (Tacmach.New.pf_global id gl)
+  apply (mkVar id)
 end }
 
 let timing timer_name f arg = f arg
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 7412de1e8..ba8356b52 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -456,39 +456,56 @@ let quote_terms env sigma ivs lc =
   term. Ring for example needs that, but Ring doesn't use Quote
   yet. *)
 
+let pf_constrs_of_globals l =
+  let rec aux l acc =
+    match l with
+      [] -> Proofview.tclUNIT (List.rev acc)
+    | hd :: tl ->
+       Tacticals.New.pf_constr_of_global hd >>= fun g -> aux tl (g :: acc)
+  in aux l []
+
 let quote f lid =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let sigma = Tacmach.New.project gl in
-    let f = Tacmach.New.pf_global f gl in
-    let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in
-    let ivs = compute_ivs f cl gl in
-    let concl = Proofview.Goal.concl gl in
-    let quoted_terms = quote_terms env sigma ivs [concl] in
-    let (p, vm) = match quoted_terms with
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let fg = Tacmach.New.pf_global f gl in
+    let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+    Tacticals.New.pf_constr_of_global fg >>= fun f ->
+    pf_constrs_of_globals clg >>= fun cl ->
+    Proofview.Goal.nf_enter { enter = begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Tacmach.New.project gl in
+      let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in
+      let concl = Proofview.Goal.concl gl in
+      let quoted_terms = quote_terms env sigma ivs [concl] in
+      let (p, vm) = match quoted_terms with
       | [p], vm -> (p,vm)
       | _ -> assert false
-    in
-    match ivs.variable_lhs with
-    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
-    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
+      in
+      match ivs.variable_lhs with
+      | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
+      | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
+    end }
   end }
 
 let gen_quote cont c f lid =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let env = Proofview.Goal.env gl in
-  let sigma = Tacmach.New.project gl in
-  let f = Tacmach.New.pf_global f gl in
-  let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in
-  let ivs = compute_ivs f cl gl in
-  let quoted_terms = quote_terms env sigma ivs [c] in
-  let (p, vm) = match quoted_terms with
-    | [p], vm -> (p,vm)
-    | _ -> assert false
-  in
-  match ivs.variable_lhs with
-    | None -> cont (mkApp (f, [| p |]))
-    | Some _ -> cont (mkApp (f, [| vm; p |]))
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let fg = Tacmach.New.pf_global f gl in
+    let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+    Tacticals.New.pf_constr_of_global fg >>= fun f ->
+    pf_constrs_of_globals clg >>= fun cl ->
+    Proofview.Goal.nf_enter { enter = begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Tacmach.New.project gl in
+      let cl = List.map (EConstr.to_constr sigma) cl in
+      let ivs = compute_ivs f cl gl in
+      let quoted_terms = quote_terms env sigma ivs [c] in
+      let (p, vm) = match quoted_terms with
+        | [p], vm -> (p,vm)
+        | _ -> assert false
+      in
+      match ivs.variable_lhs with
+      | None -> cont (mkApp (f, [| p |]))
+      | Some _ -> cont (mkApp (f, [| vm; p |]))
+    end }
   end }
 
 (*i
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 97c5cda77..66d91c634 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -75,7 +75,7 @@ let pf_get_new_ids ids gls =
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
 
-let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id)
+let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
@@ -171,7 +171,7 @@ module New = struct
     (** We only check for the existence of an [id] in [hyps] *)
     let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
-    EConstr.of_constr (Constrintern.construct_reference hyps id)
+    Constrintern.construct_reference hyps id
 
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e6e60e27f..1172e55ac 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -100,7 +100,7 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
   val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a
-  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr
+  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> Globnames.global_reference
   (** FIXME: encapsulate the level in an existential type. *)
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c1d64cfe..036173c6d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1765,12 +1765,11 @@ let vernac_locate = let open Feedback in function
 let vernac_register id r =
  if Pfedit.refining () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
-  let t = (Constrintern.global_reference (snd id)) in
-  if not (isConst t) then
+  let kn = Constrintern.global_reference (snd id) in
+  if not (isConstRef kn) then
     user_err Pp.(str "Register inline: a constant is expected");
-  let kn = destConst t in
   match r with
-  | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
+  | RegisterInline -> Global.register_inline (destConstRef kn)
 
 (********************)
 (* Proof management *)