Cleanup: removal of constr_of_global.

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

3 files changed, 46 insertions, 43 deletions

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