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

4 files changed, 13 insertions, 10 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index cf47abf445..45dd6f1ec1 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -55,7 +55,7 @@ let declare_class g =
 (** TODO: add subinstances *)
 let existing_instance glob g pri =
   let c = global g in
-  let instance = Typing.type_of (Global.env ()) Evd.empty (Universes.constr_of_global c) in
+  let instance = Global.type_of_global_unsafe c in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
       | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob 
@@ -356,7 +356,7 @@ let context l =
       let impl = List.exists test impls in
       let decl = (Discharge, (Flags.use_polymorphic_flag ()), Definitional) in
       let nstatus =
-        snd (Command.declare_assumption false decl (t, uctx) [] impl
+        pi3 (Command.declare_assumption false decl (t, uctx) [] impl
           Vernacexpr.NoInline (Loc.ghost, id))
       in
       status && nstatus
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e8d2eda8a7..3f2a518886 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -202,7 +202,7 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma
   let r = VarRef ident in
   let () = Typeclasses.declare_instance None true r in
   let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
-  (r,true)
+  (r,Univ.Instance.empty,true)
 
 | Global | Local | Discharge ->
   let local = get_locality ident local in
@@ -219,7 +219,7 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma
   let () = assumption_message ident in
   let () = Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr local p in
-  (gr,Lib.is_modtype_strict ())
+  (gr,Univ.UContext.instance ctx,Lib.is_modtype_strict ())
 
 let declare_assumptions_hook = ref ignore
 let set_declare_assumptions_hook = (:=) declare_assumptions_hook
@@ -234,8 +234,8 @@ let interp_assumption evdref env bl c =
 let declare_assumptions idl is_coe k c imps impl_is_on nl =
   let refs, status =
     List.fold_left (fun (refs,status) id ->
-      let ref',status' = declare_assumption is_coe k c imps impl_is_on nl id in
-      ref'::refs, status' && status) ([],true) idl in
+      let ref',u',status' = declare_assumption is_coe k c imps impl_is_on nl id in
+      (ref',u')::refs, status' && status) ([],true) idl in
   List.rev refs, status
 
 let do_assumptions kind nl l =
@@ -251,8 +251,11 @@ let do_assumptions kind nl l =
   snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) ->
     let t = replace_vars subst t in
     let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) imps false nl in
-    let subst' = List.map2 (fun (_,id) c -> (id,Universes.constr_of_global c)) idl refs in
-    (subst'@subst, status' && status)) ([],true) l)
+    let subst' = List.map2 
+      (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) (*FIXME incorrect should also enrich the context of the current assumption with c's context *)
+      idl refs 
+    in
+      (subst'@subst, status' && status)) ([],true) l)
 
 (* 3a| Elimination schemes for mutual inductive definitions *)
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b2ba23ef2d..d2e601edd5 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -52,7 +52,7 @@ val declare_assumption : coercion_flag -> assumption_kind ->
   types Univ.in_universe_context_set ->
   Impargs.manual_implicits ->
   bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
-  global_reference * bool
+  global_reference * Univ.Instance.t * bool
 
 val do_assumptions : locality * polymorphic * assumption_object_kind ->
   Vernacexpr.inline -> simple_binder with_coercion list -> bool
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2e9bfedc78..02e59a2278 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -835,7 +835,7 @@ let vernac_set_end_tac tac =
 
 let vernac_set_used_variables e =
   let tys =
-    List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
+    List.map fst (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
   let l = Proof_using.process_expr (Global.env ()) e tys in
   let vars = Environ.named_context (Global.env ()) in
   List.iter (fun id ->