Correct rebase on STM code. Thanks to E. Tassi for help on dealing with

latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.

- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-

7 files changed, 48 insertions, 45 deletions

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 5631488728..9ae8fcbf67 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -78,7 +78,8 @@ let gen_ground_tac flag taco ids bases gl=
 	  | None-> snd (default_solver ()) in
       let startseq gl=
 	let seq=empty_seq !ground_depth in
-	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
+        let seq,gl = extend_with_ref_list ids seq gl in
+        extend_with_auto_hints bases seq gl in
       let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in
 	qflag:=backup;result
     with reraise -> qflag:=backup;raise reraise
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index e0f4fa95f3..3faf7f8021 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -119,5 +119,6 @@ let ground_tac solver startseq gl=
 		  end
 	    with Heap.EmptyHeap->solver
       end gl in
-    wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
+    let seq, gl' = startseq gl in
+    wrap (List.length (pf_hyps gl)) true (toptac []) seq gl'
 
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 8b2ba20c17..f4a6ff48ae 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -7,5 +7,5 @@
 (************************************************************************)
 
 val ground_tac:     Tacmach.tactic ->
-  (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
+  (Proof_type.goal Tacmach.sigma -> Sequent.t * Proof_type.goal Tacmach.sigma) -> Tacmach.tactic
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index c6db6a49fb..11b120c415 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -101,14 +101,12 @@ let dummy_constr=mkMeta (-1)
 
 let dummy_bvid=Id.of_string "x"
 
-let constr_of_global = Universes.constr_of_global
-
-let mk_open_instance id gl m t=
+let mk_open_instance id idc gl m t=
   let env=pf_env gl in
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_type_of gl (constr_of_global id) in
+      let typ=pf_type_of gl idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
@@ -146,9 +144,10 @@ let left_instance_tac (inst,id) continue seq=
 	  tclTHENS (Proofview.V82.of_tactic (cut dom))
 	    [tclTHENLIST
 	       [Proofview.V82.of_tactic introf;
+                pf_constr_of_global id (fun idc ->
 		(fun gls->generalize
-		   [mkApp(constr_of_global id,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
+		   [mkApp(idc,
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls));
 		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
@@ -159,14 +158,16 @@ let left_instance_tac (inst,id) continue seq=
 	else
 	  let special_generalize=
 	    if m>0 then
-	      fun gl->
-		let (rc,ot)= mk_open_instance id gl m t in
-		let gt=
-		  it_mkLambda_or_LetIn
-		    (mkApp(constr_of_global id,[|ot|])) rc in
-		  generalize [gt] gl
+	      pf_constr_of_global id (fun idc ->
+		fun gl->
+		  let (rc,ot) = mk_open_instance id idc gl m t in
+		  let gt=
+		    it_mkLambda_or_LetIn
+		      (mkApp(idc,[|ot|])) rc in
+		    generalize [gt] gl)
 	    else
-	      generalize [mkApp(constr_of_global id,[|t|])]
+	      pf_constr_of_global id (fun idc ->
+		generalize [mkApp(idc,[|t|])])
 	  in
 	    tclTHENLIST
 	      [special_generalize;
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 31a1e6cb00..996deb8c5d 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -53,19 +53,19 @@ let clear_global=function
     VarRef id->clear [id]
   | _->tclIDTAC
 
-let constr_of_global = Universes.constr_of_global
 (* connection rules *)
 
 let axiom_tac t seq=
-  try exact_no_check (constr_of_global (find_left t seq))
+  try pf_constr_of_global (find_left t seq) exact_no_check
   with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq=
   tclIFTHENELSE
     (try
       tclTHENLIST
-	[generalize [mkApp(constr_of_global id,
-			   [|constr_of_global (find_left a seq)|])];
+	[pf_constr_of_global (find_left a seq) (fun left ->
+	  pf_constr_of_global id (fun id -> 
+	    generalize [mkApp(id, [|left|])]));
 	 clear_global id;
 	 Proofview.V82.of_tactic intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -92,7 +92,7 @@ let left_and_tac ind backtrack id continue seq gls=
  let n=(construct_nhyps ind gls).(0) in
    tclIFTHENELSE
      (tclTHENLIST
-      [Proofview.V82.of_tactic (simplest_elim (constr_of_global id));
+      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
        clear_global id;
        tclDO n (Proofview.V82.of_tactic intro)])
      (wrap n false continue seq)
@@ -106,12 +106,12 @@ let left_or_tac ind backtrack id continue seq gls=
        tclDO n (Proofview.V82.of_tactic intro);
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (Proofview.V82.of_tactic (simplest_elim (constr_of_global id)))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
       (Array.map f v)
       backtrack gls
 
 let left_false_tac id=
-  Proofview.V82.of_tactic (simplest_elim (constr_of_global id))
+  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
 
 (* left arrow connective rules *)
 
@@ -120,29 +120,28 @@ let left_false_tac id=
 let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
      let rcs=ind_hyps 0 indu largs gl in
      let vargs=Array.of_list largs in
-	     (* construire le terme  H->B, le generaliser etc *)
-     let myterm i=
+             (* construire le terme  H->B, le generaliser etc *)
+     let myterm idc i=
        let rc=rcs.(i) in
        let p=List.length rc in
        let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in
        let vars=Array.init p (fun j->mkRel (p-j)) in
        let capply=mkApp ((lift p cstr),vars) in
-       let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
-	 it_mkLambda_or_LetIn head rc in
+       let head=mkApp ((lift p idc),[|capply|]) in
+         it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
-       let newhyps=List.init lp myterm in
+       let newhyps idc =List.init lp (myterm idc) in
 	 tclIFTHENELSE
 	   (tclTHENLIST
-	      [generalize newhyps;
+	      [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
 	       clear_global id;
 	       tclDO lp (Proofview.V82.of_tactic intro)])
 	   (wrap lp false continue seq) backtrack gl
 
 let ll_arrow_tac a b c backtrack id continue seq=
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
-  let d=mkLambda (Anonymous,b,
-		  mkApp ((constr_of_global id),
-			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+  let d idc =mkLambda (Anonymous,b,
+		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
       (tclTHENS (Proofview.V82.of_tactic (cut c))
 	 [tclTHENLIST
@@ -150,9 +149,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	     clear_global id;
 	     wrap 1 false continue seq];
 	  tclTHENS (Proofview.V82.of_tactic (cut cc))
-            [exact_no_check (constr_of_global id);
+            [pf_constr_of_global id exact_no_check;
 	     tclTHENLIST
-	       [generalize [d];
+	       [pf_constr_of_global id (fun idc -> generalize [d idc]);
 		clear_global id;
 		Proofview.V82.of_tactic introf;
 		Proofview.V82.of_tactic introf;
@@ -175,7 +174,7 @@ let forall_tac backtrack continue seq=
 let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in
     tclIFTHENELSE
-      (Proofview.V82.of_tactic (simplest_elim (constr_of_global id)))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
       (tclTHENLIST [clear_global id;
                     tclDO n (Proofview.V82.of_tactic intro);
                     (wrap (n-1) false continue seq)])
@@ -187,10 +186,11 @@ let ll_forall_tac prod backtrack id continue seq=
     (tclTHENS (Proofview.V82.of_tactic (cut prod))
        [tclTHENLIST
 	  [Proofview.V82.of_tactic intro;
+           pf_constr_of_global id (fun idc ->
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
-	      let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
-		tclTHEN (generalize [term]) (clear [id0]) gls);
+              let term=mkApp(idc,[|mkVar(id0)|]) in
+		tclTHEN (generalize [term]) (clear [id0]) gls));
 	   clear_global id;
 	   Proofview.V82.of_tactic intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index c0e5c7e581..43bb6dbbf8 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -196,13 +196,13 @@ let expand_constructor_hints =
     | gr ->
 	[gr])
 
-let extend_with_ref_list l seq gl=
+let extend_with_ref_list l seq gl =
   let l = expand_constructor_hints l in
-  let f gr seq=
-    let c=Universes.constr_of_global gr in
+  let f gr (seq,gl) =
+    let gl, c = pf_eapply Evd.fresh_global gl gr in
     let typ=(pf_type_of gl c) in
-      add_formula Hyp gr typ seq gl in
-    List.fold_right f l seq
+      (add_formula Hyp gr typ seq gl,gl) in
+    List.fold_right f l (seq,gl)
 
 open Auto
 
@@ -227,7 +227,7 @@ let extend_with_auto_hints l seq gl=
 	error ("Firstorder: "^dbname^" : No such Hint database") in
       Hint_db.iter g hdb in
     List.iter h l;
-    !seqref
+    !seqref, gl (*FIXME: forgetting about universes*)
 
 let print_cmap map=
   let print_entry c l s=
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 536ee7cc34..40aa169ab2 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -54,9 +54,9 @@ val take_formula : t -> Formula.t * t
 val empty_seq : int -> t
 
 val extend_with_ref_list : global_reference list ->
-  t -> Proof_type.goal sigma -> t
+  t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
 
 val extend_with_auto_hints : Auto.hint_db_name list ->
-  t -> Proof_type.goal sigma -> t
+  t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
 
 val print_cmap: global_reference list CM.t -> Pp.std_ppcmds