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.

7 files changed, 45 insertions, 33 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index e0dff3739d..8d1e0e507a 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -472,8 +472,9 @@ let unfold_head env sigma (ids, csts) c =
 	(match Environ.named_body id env with
 	| Some b -> true, EConstr.of_constr b
 	| None -> false, c)
-    | Const (cst,u as c) when Cset.mem cst csts ->
-	true, EConstr.of_constr (Environ.constant_value_in env c)
+    | Const (cst, u) when Cset.mem cst csts ->
+        let u = EInstance.kind sigma u in
+	true, EConstr.of_constr (Environ.constant_value_in env (cst, u))
     | App (f, args) ->
 	(match aux f with
 	| true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 53b468bff7..7ae7446c82 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -746,6 +746,7 @@ let find_positions env sigma t1 t2 =
 	    let _,rargs2 = List.chop nparams args2 in
             let (mib,mip) = lookup_mind_specif env ind1 in
             let params1 = List.map EConstr.Unsafe.to_constr params1 in
+            let u1 = EInstance.kind sigma u1 in
             let ctxt = (get_constructor ((ind1,u1),mib,mip,params1) i1).cs_args in
             let adjust i = CVars.adjust_rel_to_rel_context ctxt (i+1) - 1 in
             List.flatten
@@ -1324,19 +1325,19 @@ let inject_if_homogenous_dependent_pair ty =
         hd2,ar2 = decompose_app_vect sigma t2 in
     if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit;
     if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit;
-    let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
+    let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
     (* check if the user has declared the dec principle *)
     (* and compare the fst arguments of the dep pair *)
     (* Note: should work even if not an inductive type, but the table only *)
     (* knows inductive types *)
-    if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
+    if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let inj2 = EConstr.of_constr inj2 in
-    let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
+    let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
       [Proofview.tclEFFECTS eff;
@@ -1783,6 +1784,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let select_equation_name decl =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
+        let u = EInstance.kind sigma u in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
@@ -1834,6 +1836,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let test (_,c) =
     try
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+      let u = EInstance.kind sigma u in
       let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 8e4654c02b..851554b832 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -144,6 +144,7 @@ let match_with_tuple sigma t =
   let t = match_with_one_constructor sigma None false true t in
   Option.map (fun (hd,l) ->
     let ind = destInd sigma hd in
+    let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
     let (mib,mip) = Global.lookup_pinductive ind in
     let isrec = mis_is_recursive (fst ind,mib,mip) in
     (hd,l,isrec)) t
@@ -200,8 +201,8 @@ let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
 let match_with_empty_type sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
-    | Ind ind ->
-        let (mib,mip) = Global.lookup_pinductive ind in
+    | Ind (ind, _) ->
+        let (mib,mip) = Global.lookup_inductive ind in
         let nconstr = Array.length mip.mind_consnames in
 	if Int.equal nconstr 0 then Some hdapp else None
     | _ ->  None
@@ -214,8 +215,8 @@ let is_empty_type sigma t = op2bool (match_with_empty_type sigma t)
 let match_with_unit_or_eq_type sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
-    | Ind ind  ->
-        let (mib,mip) = Global.lookup_pinductive ind in
+    | Ind (ind , _) ->
+        let (mib,mip) = Global.lookup_inductive ind in
         let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
         let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
@@ -369,8 +370,8 @@ let is_forall_term sigma c = op2bool (match_with_forall_term sigma c)
 let match_with_nodep_ind sigma t =
   let (hdapp,args) = decompose_app sigma t in
     match EConstr.kind sigma hdapp with
-      | Ind ind  ->
-          let (mib,mip) = Global.lookup_pinductive ind in
+      | Ind (ind, _)  ->
+          let (mib,mip) = Global.lookup_inductive ind in
 	    if Array.length (mib.mind_packets)>1 then None else
 	      let nodep_constr c = has_nodep_prod_after mib.mind_nparams sigma (EConstr.of_constr c) in
 		if Array.for_all nodep_constr mip.mind_nf_lc then
@@ -387,8 +388,8 @@ let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t)
 let match_with_sigma_type sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
-    | Ind ind  ->
-        let (mib,mip) = Global.lookup_pinductive ind in
+    | Ind (ind, _) ->
+        let (mib,mip) = Global.lookup_inductive ind in
           if Int.equal (Array.length (mib.mind_packets)) 1 &&
 	    (Int.equal mip.mind_nrealargs 0) &&
 	    (Int.equal (Array.length mip.mind_consnames)1) &&
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index c46817f505..dd09c3a4d7 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -122,19 +122,19 @@ val match_with_equation:
 (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] 
    Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
 val find_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr ->
-      coq_eq_data * Univ.universe_instance * (types * constr * constr)
+      coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
 val find_this_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr ->
-      coq_eq_data * Univ.universe_instance * (types * constr * constr)
+      coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
-val find_eq_data : evar_map -> constr -> coq_eq_data * Univ.universe_instance * equation_kind
+val find_eq_data : evar_map -> constr -> coq_eq_data * EInstance.t * equation_kind
 
 (** Match a term of the form [(existT A P t p)] 
    Returns associated lemmas and [A,P,t,p] *)
 val find_sigma_data_decompose : evar_map -> constr ->
-  coq_sigma_data * (Univ.universe_instance * constr * constr * constr * constr)
+  coq_sigma_data * (EInstance.t * constr * constr * constr * constr)
 
 (** Match a term of the form [{x:A|P}], returns [A] and [P] *)
 val match_sigma : evar_map -> constr -> constr * constr
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index a1cd510475..90b7d6581a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -606,6 +606,7 @@ module New = struct
       isrec allnames tac predicate ind (c, t) =
     Proofview.Goal.enter { enter = begin fun gl ->
     let sigma, elim = (mk_elim ind).enter gl in
+    let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (Proofview.Goal.enter { enter = begin fun gl ->
     let indclause = mk_clenv_from gl (c, t) in
@@ -680,17 +681,19 @@ module New = struct
     (sigma, EConstr.of_constr c)
   end }
 
-  let gl_make_case_dep ind = { enter = begin fun gl ->
+  let gl_make_case_dep (ind, u) = { enter = begin fun gl ->
     let sigma = Sigma.Unsafe.of_evar_map (project gl) in
-    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
+    let u = EInstance.kind (project gl) u in
+    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true
       (elimination_sort_of_goal gl)
     in
     (Sigma.to_evar_map sigma, EConstr.of_constr r)
   end }
 
-  let gl_make_case_nodep ind = { enter = begin fun gl ->
+  let gl_make_case_nodep (ind, u) = { enter = begin fun gl ->
     let sigma = Sigma.Unsafe.of_evar_map (project gl) in
-    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
+    let u = EInstance.kind (project gl) u in
+    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false
       (elimination_sort_of_goal gl)
     in
     (Sigma.to_evar_map sigma, EConstr.of_constr r)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 5839666a73..3b90ec514a 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -124,7 +124,7 @@ val fix_empty_or_and_pattern : int ->
   delayed_open_constr or_and_intro_pattern_expr ->
   delayed_open_constr or_and_intro_pattern_expr
 
-val compute_constructor_signatures : rec_flag -> pinductive -> bool list array
+val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array
 
 (** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
@@ -256,11 +256,11 @@ module New : sig
 
   val case_then_using :
     or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    constr option -> pinductive -> constr * types -> unit Proofview.tactic
+    constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
 
   val case_nodep_then_using :
     or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    constr option -> pinductive -> constr * types -> unit Proofview.tactic
+    constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
 
   val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
   val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 55d6df6596..8306ac1740 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1445,6 +1445,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
   let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in
   let sort = Tacticals.New.elimination_sort_of_goal gl in
+  let mind = on_snd (fun u -> EInstance.kind (Sigma.to_evar_map sigma) u) mind in
   let Sigma (elim, sigma, p) =
     if occur_term (Sigma.to_evar_map sigma) c concl then
       build_case_analysis_scheme env sigma mind true sort
@@ -1647,6 +1648,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
 	let elim =
 	  try DefinedRecord (Recordops.lookup_projections ind)
 	  with Not_found ->
+            let u = EInstance.kind sigma u in
             let sigma = Sigma.Unsafe.of_evar_map sigma in
 	    let Sigma (elim, _, _) = build_case_analysis_scheme env sigma (ind,u) false sort in
 	    let elim = EConstr.of_constr elim in
@@ -2214,9 +2216,9 @@ let constructor_tac with_evars expctdnumopt i lbind =
       Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
       check_number_of_constructors expctdnumopt i nconstr;
 
-      let Sigma (cons, sigma, p) = Sigma.fresh_constructor_instance
+      let Sigma ((cons, u), sigma, p) = Sigma.fresh_constructor_instance
 	(Proofview.Goal.env gl) sigma (fst mind, i) in
-      let cons = mkConstructU cons in
+      let cons = mkConstructU (cons, EInstance.make u) in
 	
       let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in
       let tac =
@@ -4033,24 +4035,25 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
 
 let guess_elim isrec dep s hyp0 gl =
   let tmptyp0 =	Tacmach.New.pf_get_hyp_typ hyp0 gl in
-  let mind,_ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
+  let (mind, u), _ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
   let evd, elimc =
-    if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl
+    if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl
     else
       let env = Tacmach.New.pf_env gl in
       let sigma = Sigma.Unsafe.of_evar_map (Tacmach.New.project gl) in
+      let u = EInstance.kind (Tacmach.New.project gl) u in
       if use_dependent_propositions_elimination () && dep
       then
-        let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma mind true s in
+        let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma (mind, u) true s in
         let ind = EConstr.of_constr ind in
         (Sigma.to_evar_map sigma, ind)
       else
-        let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma mind s in
+        let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma (mind, u) s in
         let ind = EConstr.of_constr ind in
         (Sigma.to_evar_map sigma, ind)
   in
   let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
-    evd, ((elimc, NoBindings), elimt), mkIndU mind
+    evd, ((elimc, NoBindings), elimt), mkIndU (mind, u)
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let sigma = Tacmach.New.project gl in
@@ -4637,9 +4640,10 @@ let case_type t =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let env = Tacmach.New.pf_env gl in
-  let (ind,t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in
+  let ((ind, u), t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in
+  let u = EInstance.kind (Sigma.to_evar_map sigma) u in
   let s = Tacticals.New.elimination_sort_of_goal gl in
-  let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma ind s in
+  let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma (ind, u) s in
   let elimc = EConstr.of_constr elimc in
   Sigma (elim_scheme_type elimc t, evd, p)
   end }