Merge PR#696: Trunk+cleanup constr of global

8 files changed, 79 insertions, 72 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b3017f359..43c06a54d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -231,9 +231,9 @@ let make_prb gls depth additionnal_terms =
 let build_projection intype (cstr:pconstructor) special default gls=
   let open Tacmach.New in
   let ci= (snd(fst cstr)) in
-  let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+  let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
   let id=pf_get_new_id (Id.of_string "t") gls in
-    mkLambda(Name id,intype,body)
+  sigma, mkLambda(Name id,intype,body)
 
 (* generate an adhoc tactic following the proof tree  *)
 
@@ -346,12 +346,13 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let special=mkRel (1+nargs-argind) in
 	 refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
-         let proj =
+         let sigma, proj =
            build_projection intype cstr special default gl
          in
 	 let injt=
            app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
-	   Tacticals.New.tclTHEN injt (proof_tac prf)))
+	 Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+                               (Tacticals.New.tclTHEN injt (proof_tac prf))))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end }
 
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/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cba9c1364..9726a5b40 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -306,7 +306,8 @@ let project_hint pri l2r r =
     | _ -> assert false in
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let p = EConstr.of_constr @@ Universes.constr_of_global p in
+  let sigma, p = Evd.fresh_global env sigma p in
+  let p = EConstr.of_constr p in
   let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
@@ -735,7 +736,6 @@ let rewrite_except h =
 
 let refl_equal = 
   let coq_base_constant s =
-    Universes.constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition"
       (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in
   function () -> (coq_base_constant "eq_refl")
@@ -747,8 +747,9 @@ let refl_equal =
 let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.enter { enter = begin fun gl ->
     let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in
-       Tacticals.New.tclTHENLIST
-         [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))];
+    Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req ->
+    Tacticals.New.tclTHENLIST
+         [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))];
           Proofview.Goal.enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 966b11d0e..dadcfb9f2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -751,17 +751,23 @@ let default_flags = { under_lambdas = true; on_morphisms = true; }
 
 let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None
 
-let make_eq () =
-(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
-let make_eq_refl () =
-(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ()))
+let new_global (evars, cstrs) gr = 
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map evars) gr
+  in (Sigma.to_evar_map sigma, cstrs), c
 
-let get_rew_prf r = match r.rew_prf with
-  | RewPrf (rel, prf) -> rel, prf 
+let make_eq sigma =
+  new_global sigma (Coqlib.build_coq_eq ())
+let make_eq_refl sigma =
+  new_global sigma (Coqlib.build_coq_eq_refl ())
+
+let get_rew_prf evars r = match r.rew_prf with
+  | RewPrf (rel, prf) -> evars, (rel, prf)
   | RewCast c ->
-    let rel = mkApp (make_eq (), [| r.rew_car |]) in
-      rel, mkCast (mkApp (make_eq_refl (), [| r.rew_car; r.rew_from |]),
-		   c, mkApp (rel, [| r.rew_from; r.rew_to |]))
+    let evars, eq = make_eq evars in
+    let evars, eq_refl = make_eq_refl evars in
+    let rel = mkApp (eq, [| r.rew_car |]) in
+    evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]),
+		         c, mkApp (rel, [| r.rew_from; r.rew_to |])))
 
 let poly_subrelation sort = 
   if sort then PropGlobal.subrelation else TypeGlobal.subrelation
@@ -827,7 +833,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 		      env evars carrier relation x in
 		    [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
 	      | Some r ->
-		  [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, 
+                 let evars, proof = get_rew_prf evars r in
+		 [ snd proof; r.rew_to; x ] @ acc, subst, evars, 
 	      sigargs, r.rew_to :: typeargs')
 	  | None ->
 	      if not (Option.is_empty y) then 
@@ -847,7 +854,8 @@ let apply_constraint env avoid car rel prf cstr res =
   | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res
 
 let coerce env avoid cstr res = 
-  let rel, prf = get_rew_prf res in
+  let evars, (rel, prf) = get_rew_prf res.rew_evars res in
+  let res = { res with rew_evars = evars } in
     apply_constraint env avoid res.rew_car rel prf cstr res
 
 let apply_rule unify loccs : int pure_strategy =
@@ -868,8 +876,7 @@ let apply_rule unify loccs : int pure_strategy =
 	    else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
 	    else
 	      let res = { rew with rew_car = ty } in
-              let rel, prf = get_rew_prf res in
-	      let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in
+	      let res = Success (coerce env unfresh cstr res) in
               (occ, res)
     }
 
@@ -1231,9 +1238,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	in 
 	let res = 
 	  match res with
-	  | Success r ->  
-	    let rel, prf = get_rew_prf r in
-	      Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r)
+	  | Success r -> Success (coerce env unfresh (prop,cstr) r)
 	  | Fail | Identity -> res
 	in state, res
       | _ -> state, Fail
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index f5e6f05ce..2858df313 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -14,7 +14,6 @@ open Stdarg
 open Tacarg
 open Misctypes
 open Globnames
-open Term
 open Genredexpr
 open Patternops
 
@@ -91,7 +90,7 @@ open Printer
 let subst_global_reference subst =
  let subst_global ref =
   let ref',t' = subst_global subst ref in
-   if not (eq_constr (Universes.constr_of_global ref') t') then
+   if not (is_global ref' t') then
     Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
           str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
           pr_global ref') ;
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 4ec111e01..d8e21d81d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -220,9 +220,7 @@ let apply_nnpp _ ist =
   Proofview.tclBIND
     (Proofview.tclUNIT ())
     begin fun () -> try
-      let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in
-      let nnpp = EConstr.of_constr nnpp in
-      apply nnpp
+      Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply
     with Not_found -> tclFAIL 0 (Pp.mt ())
     end
 
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