Rework handling of universes on top of the STM, allowing for delayed

computation in case of non-polymorphic proofs. Also fix plugins after
forgotten merge conflicts. Still does not compile everything.

4 files changed, 33 insertions, 47 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 2adc82505..88693c196 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -340,19 +340,7 @@ let generate_functional_principle
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let value = change_property_sort s new_principle_type new_princ_name in
 	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce =
-          { const_entry_body =
-              Future.from_val (value,Declareops.no_seff);
-            const_entry_secctx = None;
-	    const_entry_type = None;	
-	    const_entry_polymorphic = false;
-	    const_entry_universes = Univ.UContext.empty (*FIXME*);
-	    const_entry_proj = None;
-	    const_entry_opaque = false;
-            const_entry_feedback = None;
-	    const_entry_inline_code = false
-	  }
-	in
+	let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *)
 	ignore(
 	  Declare.declare_constant
 	    name
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 7ed8e03a9..ae05fbdc3 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -152,18 +152,10 @@ let ty c = Typing.type_of (Global.env()) Evd.empty c
 let decl_constant na ctx c =
   let vars = Universes.universes_of_constr c in
   let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
-  mkConst(declare_constant (Id.of_string na) (DefinitionEntry
-    { const_entry_body = Future.from_val (c, Declareops.no_seff);
-      const_entry_secctx = None;
-      const_entry_type = None;
-      const_entry_polymorphic = false;
-      const_entry_universes = Univ.ContextSet.to_context ctx;
-      const_entry_proj = None;
-      const_entry_opaque = true;
-      const_entry_inline_code = false;
-      const_entry_feedback = None;
-    },
-    IsProof Lemma))
+  mkConst(declare_constant (Id.of_string na) 
+	    (DefinitionEntry (definition_entry ~opaque:true
+				~univs:(Univ.ContextSet.to_context ctx) c),
+	     IsProof Lemma))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
@@ -442,11 +434,11 @@ let theory_to_obj : ring_info -> obj =
 
 let setoid_of_relation env evd a r =
   try
-    let evm = !evd, Int.Set.empty in
-    let evm, refl = Rewrite.PropGlobal.get_reflexive_proof env evm a r in
-    let evm, sym = Rewrite.PropGlobal.get_symmetric_proof env evm a r in
-    let evm, trans = Rewrite.PropGlobal.get_transitive_proof env evm a r in
-      evd := fst evm;
+    let evm = !evd in
+    let evm, refl = Rewrite.get_reflexive_proof env evm a r in
+    let evm, sym = Rewrite.get_symmetric_proof env evm a r in
+    let evm, trans = Rewrite.get_transitive_proof env evm a r in
+      evd := evm;
       lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
   with Not_found ->
     error "cannot find setoid relation"
@@ -682,9 +674,9 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
   let lemma2 = params.(4) in
 
   let lemma1 =
-    decl_constant (Id.to_string name^"_ring_lemma1") ctx (Future.from_val ( lemma1,Declareops.no_seff)) in
+    decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in
   let lemma2 =
-    decl_constant (Id.to_string name^"_ring_lemma2") ctx (Future.from_val ( lemma2,Declareops.no_seff)) in
+    decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
@@ -724,10 +716,16 @@ type 'constr ring_mod =
   | Div_spec of Constrexpr.constr_expr
 
 
+let ic_coeff_spec = function
+  | Computational t -> Computational (ic_unsafe t)
+  | Morphism t -> Morphism (ic_unsafe t)
+  | Abstract -> Abstract
+
+
 VERNAC ARGUMENT EXTEND ring_mod
-  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic_unsafe eq_test)) ]
+  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ]
   | [ "abstract" ] -> [ Ring_kind Abstract ]
-  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic_unsafe morph)) ]
+  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ]
   | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
   | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
   | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
@@ -754,7 +752,7 @@ let process_ring_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_kind k -> set_once "ring kind" kind k
+      Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k)
     | Const_tac t -> set_once "tactic recognizing constants" cst_tac t
     | Pre_tac t -> set_once "preprocess tactic" pre t
     | Post_tac t -> set_once "postprocess tactic" post t
@@ -1026,18 +1024,18 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power
   let lemma4 = params.(6) in
   let cond_lemma =
     match inj with
-      | Some thm -> mkApp(constr_of params.(8),[|thm|])
-      | None -> constr_of params.(7) in
+      | Some thm -> mkApp(params.(8),[|thm|])
+      | None -> params.(7) in
   let lemma1 = decl_constant (Id.to_string name^"_field_lemma1")
-    ctx (Future.from_val (lemma1,Declareops.no_seff)) in
+    ctx lemma1 in
   let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") 
-    ctx (Future.from_val (lemma2,Declareops.no_seff)) in
+    ctx lemma2 in
   let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") 
-    ctx (Future.from_val (lemma3,Declareops.no_seff)) in
+    ctx lemma3 in
   let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") 
-    ctx (Future.from_val (lemma4,Declareops.no_seff)) in
+    ctx lemma4 in
   let cond_lemma = decl_constant (Id.to_string name^"_lemma5") 
-    ctx (Future.from_val (cond_lemma,Declareops.no_seff)) in
+    ctx cond_lemma in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
@@ -1083,7 +1081,7 @@ let process_field_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_mod(Ring_kind k) -> set_once "field kind" kind k
+      Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k)
     | Ring_mod(Const_tac t) ->
         set_once "tactic recognizing constants" cst_tac t
     | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 5c060c3d6..67c9dd0a3 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -37,7 +37,7 @@ let interp_ascii dloc p =
   let rec aux n p =
      if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     GRef (dloc,if Int.equal mp 0 then glob_false else glob_true,None)
+     GRef (dloc,(if Int.equal mp 0 then glob_false else glob_true),None)
      :: (aux (n-1) (p/2)) in
   GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p)
 
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 5131a5f38..2b1410be6 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -182,8 +182,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([GRef (Loc.ghost, glob_ZERO, None, None);
-    GRef (Loc.ghost, glob_POS, None, None);
-    GRef (Loc.ghost, glob_NEG, None, None)],
+  ([GRef (Loc.ghost, glob_ZERO, None);
+    GRef (Loc.ghost, glob_POS, None);
+    GRef (Loc.ghost, glob_NEG, None)],
   uninterp_z,
   true)