Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.

11 files changed, 38 insertions, 19 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c9c904e35..2d9dec095 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -66,6 +66,7 @@ let rec decompose_term env sigma t=
 	      decompose_term env sigma b)
     | Construct c ->
 	let (((mind,i_ind),i_con),u)= c in 
+	let u = EInstance.kind sigma u in
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
@@ -75,9 +76,11 @@ let rec decompose_term env sigma t=
 		       ci_nhyps=nargs-oib.mind_nparams}
     | Ind c -> 
 	let (mind,i_ind),u = c in 
+	let u = EInstance.kind sigma u in
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
     | Const (c,u) -> 
+	let u = EInstance.kind sigma u in
 	let canon_const = constant_of_kn (canonical_con c) in 
 	  (Symb (Constr.mkConstU (canon_const,u)))
     | Proj (p, c) -> 
@@ -408,7 +411,8 @@ let build_term_to_complete uf meta pac =
   let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
   let dummy_args = List.rev (List.init pac.arity meta) in
   let all_args = List.rev_append real_args dummy_args in
-    applist (mkConstructU cinfo.ci_constr, all_args)
+  let (kn, u) = cinfo.ci_constr in
+    applist (mkConstructU (kn, EInstance.make u), all_args)
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter { enter = begin fun gl ->
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 87bac2fe3..7773f6a2f 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -91,6 +91,7 @@ let kind_of_formula gl term =
 		  Some (i,l,n)->
                     let l = List.map EConstr.Unsafe.to_constr l in
 		    let ind,u=EConstr.destInd (project gl) i in
+		    let u = EConstr.EInstance.kind (project gl) u in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
 		      if Int.equal nconstr 0 then
@@ -112,7 +113,10 @@ let kind_of_formula gl term =
 			      Or((ind,u),l,is_trivial)
 		| _ ->
 		    match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with
-			Some (i,l)-> Exists((EConstr.destInd (project gl) i),List.map EConstr.Unsafe.to_constr l)
+			Some (i,l)->
+                          let (ind, u) = EConstr.destInd (project gl) i in
+                          let u = EConstr.EInstance.kind (project gl) u in
+                          Exists((ind, u), List.map EConstr.Unsafe.to_constr l)
 		      |_-> Atom (normalize cciterm)
 
 type atoms = {positive:constr list;negative:constr list}
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e845db3bc..529b91c4c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -300,7 +300,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
       hook
   ;
     (*       let _tim1 = System.get_time ()  in *)
-      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map EConstr.mkConstU funs) mutr_nparams)));
+      let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
+      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)));
     (*       let _tim2 =  System.get_time ()  in *)
     (* 	begin *)
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 63bd3848f..8aab3b742 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1275,8 +1275,9 @@ let do_build_inductive
   let open Context.Named.Declaration in
   let evd,env =
     Array.fold_right2
-      (fun id c (evd,env) ->
-       let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in
+      (fun id (c, u) (evd,env) ->
+       let u = EConstr.EInstance.make u in
+       let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in
        let t = EConstr.Unsafe.to_constr t in
        evd,
        Environ.push_named (LocalAssum (id,t))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a7489fb7b..2852152e1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -249,7 +249,8 @@ let derive_inversion fix_names =
 	   Evd.fresh_global
 	     (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in 
         let c = EConstr.of_constr c in
-	 evd, destConst evd c::l
+        let (cst, u) = destConst evd c in
+	 evd, (cst, EInstance.kind evd u) :: l
 	)
 	fix_names
 	(evd',[])
@@ -412,7 +413,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
             let c = EConstr.of_constr c in
-	    evd,((destConst evd c)::l)
+            let (cst, u) = destConst evd c in
+            let u = EInstance.kind evd u in
+            evd,((cst, u) :: l)
 	   )
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
@@ -427,7 +430,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
             let c = EConstr.of_constr c in
-	    evd,((destConst evd c)::l)
+            let (cst, u) = destConst evd c in
+            let u = EInstance.kind evd u in
+            evd,((cst, u) :: l)
 	   )
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2c2cd919b..94ec0a898 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -783,7 +783,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
   assert (funs <> []);
   assert (graphs <> []);
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
-  let funs_constr = Array.map mkConstU funs  in
+  let map (c, u) = mkConstU (c, EInstance.make u) in
+  let funs_constr = Array.map map funs  in
   States.with_state_protection_on_exception
     (fun () ->
      let env = Global.env () in
@@ -882,7 +883,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
 	   (Array.to_list
 	      (Array.mapi
-		 (fun i _ -> ((kn,i),u(* Univ.Instance.empty *)),true,InType)
+		 (fun i _ -> ((kn,i), EInstance.kind !evd u),true,InType)
 		 mib.Declarations.mind_packets
 	      )
 	   )
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 44aacaf45..c0298d06c 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -136,13 +136,14 @@ let prNamedRLDecl s lc =
 
 let showind (id:Id.t) =
   let cstrid = Constrintern.global_reference id in
-  let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
-  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) 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);
+    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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0a288c76e..5460d6fb7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -86,9 +86,10 @@ let def_of_const t =
 
 let type_of_const sigma t =
    match (EConstr.kind sigma t) with
-   | Const sp ->
+   | Const (sp, u) ->
+      let u = EInstance.kind sigma u in
       (* FIXME discarding universe constraints *)
-      Typeops.type_of_constant_in (Global.env()) sp
+      Typeops.type_of_constant_in (Global.env()) (sp, u)
     |_ -> assert false
 
 let constr_of_global x = 
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 55108631b..b34afd51b 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1073,7 +1073,7 @@ let decompose l c =
   Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let to_ind c =
-      if isInd sigma c then Univ.out_punivs (destInd sigma c)
+      if isInd sigma c then fst (destInd sigma c)
       else error "not an inductive type"
     in
     let l = List.map to_ind l in
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 95620b374..b76009c99 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -255,7 +255,7 @@ let coerce_to_evaluable_ref env sigma v =
     | IndRef _ | ConstructRef _ -> fail ()
   else
     match Value.to_constr v with
-    | Some c when isConst sigma c -> EvalConstRef (Univ.out_punivs (destConst sigma c))
+    | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
     | Some c when isVar sigma c -> EvalVarRef (destVar sigma c)
     | _ -> fail ()
   in if Tacred.is_evaluable env ev then ev else fail ()
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 23069a9ab..fc9d70ae7 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -225,8 +225,9 @@ let compute_rhs env sigma bodyi index_of_f =
 let compute_ivs f cs gl =
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
-  let cst = try destConst sigma f with DestKO -> i_can't_do_that () in
-  let body = Environ.constant_value_in (Global.env()) cst in
+  let (cst, u) = try destConst sigma f with DestKO -> i_can't_do_that () in
+  let u = EInstance.kind sigma u in
+  let body = Environ.constant_value_in (Global.env()) (cst, u) in
   let body = EConstr.of_constr body in
   match decomp_term sigma body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->