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.
-

5 files changed, 6 insertions, 5 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 88693c196..05cdd288c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -645,7 +645,7 @@ let build_case_scheme fa =
 (*     Constrintern.global_reference  id *)
 (*   in  *)
   let funs =  (fun (_,f,_) ->
-		 try Universes.constr_of_global (Nametab.global f)
+		 try Universes.unsafe_constr_of_global (Nametab.global f)
 		 with Not_found ->
 		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
   let first_fun,u = destConst  funs in
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 3802aa365..90282fcf7 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -163,7 +163,7 @@ VERNAC COMMAND EXTEND Function
              (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
-             Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
+             Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids, false), VtLater)
          | x -> x ]
     -> [ do_generate_principle false (List.map snd recsl) ]
 END
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d98f824e8..d6ad5575b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -181,6 +181,7 @@ let is_rec names =
   let rec lookup names = function
     | GVar(_,id) -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
+    | GProj (loc, p, c) -> lookup names c
     | GCast(_,b,_) -> lookup names b
     | GProj _ -> error "GProj not handled"
     | GRec _ -> error "GRec not handled"
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8cccb0bed..5d9c226b7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -166,7 +166,7 @@ let save with_clean id const (locality,_,kind) hook =
 
 
 let cook_proof _ =
-  let (id,(entry,strength)) = Pfedit.cook_proof () in
+  let (id,(entry,_,strength)) = Pfedit.cook_proof () in
   (id,(entry,strength))
 
 let get_proof_clean do_reduce =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 96bf4c921..50e7507f4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -75,7 +75,7 @@ let type_of_const t =
     Const sp -> Typeops.type_of_constant (Global.env()) sp
     |_ -> assert false
 
-let constr_of_global = Universes.constr_of_global
+let constr_of_global = Universes.unsafe_constr_of_global
 
 let constant sl s = constr_of_global (find_reference sl s)
 
@@ -1016,7 +1016,7 @@ let compute_terminate_type nb_args func =
 		  delayed_force nat,
 		  (mkProd (Name k_id, delayed_force nat,
 			   mkArrow cond result))))|])in
-  let value = mkApp(delayed_force coq_sig,
+  let value = mkApp(constr_of_global (delayed_force coq_sig_ref),
 		    [|b;
 		      (mkLambda (Name v_id, b, nb_iter))|]) in
   compose_prod rev_args value