Merge PR#379: Introducing evar-insensitive constrs

1 files changed, 117 insertions, 101 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index d44dcf10df..7ae7446c82 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,18 +6,20 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module CVars = Vars
 open Pp
 open CErrors
 open Util
 open Names
 open Nameops
 open Term
-open Vars
 open Termops
+open Environ
+open EConstr
+open Vars
 open Namegen
 open Inductive
 open Inductiveops
-open Environ
 open Libnames
 open Globnames
 open Reductionops
@@ -144,7 +146,7 @@ let freeze_initial_evars sigma flags clause =
   (* We take evars of the type: this may include old evars! For excluding *)
   (* all old evars, including the ones occurring in the rewriting lemma, *)
   (* we would have to take the clenv_value *)
-  let newevars = Evd.evars_of_term (clenv_type clause) in
+  let newevars = Evarutil.undefined_evars_of_term sigma (clenv_type clause) in
   let evars =
     fold_undefined (fun evk _ evars ->
       if Evar.Set.mem evk newevars then evars
@@ -165,8 +167,9 @@ let side_tac tac sidetac =
 
 let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let env = Proofview.Goal.env gl in
+  let sigma = project gl in
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
-  let (equiv, args) = decompose_appvect (Clenv.clenv_type eqclause) in
+  let (equiv, args) = decompose_app_vect sigma (Clenv.clenv_type eqclause) in
   let arglen = Array.length args in
   let () = if arglen < 2 then error "The term provided is not an applied relation." in
   let c1 = args.(arglen - 2) in
@@ -304,7 +307,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
       else instantiate_lemma_all frzevars gl c t l l2r concl
     in
     let typ = match cls with
-    | None -> pf_nf_concl gl
+    | None -> pf_concl gl
     | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
     in
     let cs = instantiate_lemma typ in
@@ -326,9 +329,9 @@ let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hoo
 let jmeq_same_dom gl = function
   | None -> true (* already checked in Hipattern.find_eq_data_decompose *)
   | Some t ->
-    let rels, t = decompose_prod_assum t in
-    let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in
-    match decompose_app t with
+    let rels, t = decompose_prod_assum (project gl) t in
+    let env = push_rel_context rels (Proofview.Goal.env gl) in
+    match decompose_app (project gl) t with
       | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
       | _ -> false
 
@@ -336,6 +339,8 @@ let jmeq_same_dom gl = function
    eliminate lbeq on sort_of_gl. *)
 
 let find_elim hdcncl lft2rgt dep cls ot gl =
+  let sigma = project gl in
+  let is_global gr c = Termops.is_global sigma gr c in
   let inccl = Option.is_empty cls in
   if (is_global Coqlib.glob_eq hdcncl ||
       (is_global Coqlib.glob_jmeq hdcncl &&
@@ -343,7 +348,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
     || Flags.version_less_or_equal Flags.V8_2
   then
     let c = 
-      match kind_of_term hdcncl with 
+      match EConstr.kind sigma hdcncl with 
       | Ind (ind_sp,u) -> 
 	let pr1 = 
 	  lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) 
@@ -371,6 +376,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	assert false
     in
       let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+      let elim = EConstr.of_constr elim in
       Sigma ((elim, Safe_typing.empty_private_constants), sigma, p)
   else
   let scheme_name = match dep, lft2rgt, inccl with
@@ -385,13 +391,14 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
     | true, _, true -> rew_r2l_dep_scheme_kind
     | true, _, false -> rew_r2l_forward_dep_scheme_kind
   in
-  match kind_of_term hdcncl with
+  match EConstr.kind sigma hdcncl with
   | Ind (ind,u) -> 
       let c, eff = find_scheme scheme_name ind in 
       (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
       let Sigma (elim, sigma, p) =
 	Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
       in
+      let elim = EConstr.of_constr elim in
       Sigma ((elim, eff), sigma, p)
   | _ -> assert false
 
@@ -400,12 +407,12 @@ let type_of_clause cls gl = match cls with
   | Some id -> pf_get_hyp_typ id gl
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
-  let isatomic = isProd (whd_zeta evd hdcncl) in
+  let isatomic = isProd evd (whd_zeta evd hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
-  let dep = dep_proof_ok && dep_fun c type_of_cls in
+  let dep = dep_proof_ok && dep_fun evd c type_of_cls in
   let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
   let tac =
       Proofview.tclEFFECTS effs <*>
@@ -441,8 +448,8 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
-    let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
-      match match_with_equality_type t with
+    let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in
+      match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
@@ -455,9 +462,10 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
             end
             begin function
               | (e, info) ->
+                  Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
 	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
-	          match match_with_equality_type t' with
+	          match match_with_equality_type sigma t' with
 	            | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		  leibniz_rewrite_ebindings_clause cls lft2rgt tac c
@@ -523,7 +531,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	let do_hyps =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
 	  let ids gl =
-	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
+	    let ids_in_c = Termops.global_vars_set (Global.env()) (project gl) (fst c) in
             let ids_of_hyps = pf_ids_of_hyps gl in
 	    Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
 	  in
@@ -713,7 +721,6 @@ let _ =
       optread  = (fun () -> !keep_proof_equalities_for_injection) ;
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
-
 let find_positions env sigma t1 t2 =
   let project env sorts posn t1 t2 =
     let ty1 = get_type_of env sigma t1 in
@@ -724,7 +731,7 @@ let find_positions env sigma t1 t2 =
   let rec findrec sorts posn t1 t2 =
     let hd1,args1 = whd_all_stack env sigma t1 in
     let hd2,args2 = whd_all_stack env sigma t2 in
-    match (kind_of_term hd1, kind_of_term hd2) with
+    match (EConstr.kind sigma hd1, EConstr.kind sigma hd2) with
       | Construct ((ind1,i1 as sp1),u1), Construct (sp2,_)
           when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
             ->
@@ -738,8 +745,10 @@ let find_positions env sigma t1 t2 =
 	    let params1,rargs1 = List.chop nparams args1 in
 	    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 = Vars.adjust_rel_to_rel_context ctxt (i+1) - 1 in
+            let adjust i = CVars.adjust_rel_to_rel_context ctxt (i+1) - 1 in
             List.flatten
 	      (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
 		0 rargs1 rargs2)
@@ -850,21 +859,23 @@ let descend_then env sigma head dirn =
   let (mib,mip) = lookup_mind_specif env ind in
   let cstr = get_constructors env indf in
   let dirn_nlams = cstr.(dirn-1).cs_nargs in
-  let dirn_env = push_rel_context cstr.(dirn-1).cs_args env in
+  let dirn_env = Environ.push_rel_context cstr.(dirn-1).cs_args env in
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let deparsign = make_arity_signature env true indf in
+      let deparsign = make_arity_signature env sigma true indf in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if Int.equal i dirn then dirnval else dfltval in
-	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
+	let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.(i-1).cs_args in
+	let args = name_context env sigma cs_args in
+	it_mkLambda_or_LetIn result args in
       let brl =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
       let ci = make_case_info env ind RegularStyle in
-      Inductiveops.make_case_or_project env indf ci p head (Array.of_list brl)))
+      Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
 
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -899,17 +910,22 @@ let build_selector env sigma dirn c ind special default =
   let ind, _ = check_privacy env indp in
   let typ = Retyping.get_type_of env sigma default in
   let (mib,mip) = lookup_mind_specif env ind in
-  let deparsign = make_arity_signature env true indf in
+  let deparsign = make_arity_signature env sigma true indf in
   let p = it_mkLambda_or_LetIn typ deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
     let endpt = if Int.equal i dirn then special else default in
-    it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in
+    let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstrs.(i-1).cs_args in
+    it_mkLambda_or_LetIn endpt args in
   let brl =
     List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
   let ci = make_case_info env ind RegularStyle in
   mkCase (ci, p, c, Array.of_list brl)
 
+let build_coq_False () = EConstr.of_constr (build_coq_False ())
+let build_coq_True () = EConstr.of_constr (build_coq_True ())
+let build_coq_I () = EConstr.of_constr (build_coq_I ())
+
 let rec build_discriminator env sigma dirn c = function
   | [] ->
       let ind = get_type_of env sigma c in
@@ -935,9 +951,9 @@ let rec build_discriminator env sigma dirn c = function
 
 let gen_absurdity id =
   Proofview.Goal.enter { enter = begin fun gl ->
+  let sigma = project gl in
   let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
-  let hyp_typ = pf_nf_evar gl hyp_typ in
-  if is_empty_type hyp_typ
+  if is_empty_type sigma hyp_typ
   then
     simplest_elim (mkVar id)
   else
@@ -967,6 +983,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
   let absurd_term  = build_coq_False () in
   let eq_elim, eff = ind_scheme_of_eq lbeq in
   let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
+  let eq_elim = EConstr.of_constr eq_elim in
     sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
     eff
 
@@ -976,7 +993,7 @@ let apply_on_clause (f,t) clause =
   let sigma =  clause.evd in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv =
-    (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
+    (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _  -> user_err  (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
@@ -998,7 +1015,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     match find_positions env sigma t1 t2 with
     | Inr _ ->
@@ -1008,7 +1025,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   end }
 
 let onEquality with_evars tac (c,lbindc) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
@@ -1023,12 +1040,12 @@ let onEquality with_evars tac (c,lbindc) =
   end }
 
 let onNegatedEquality with_evars tac =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    match kind_of_term (hnf_constr env sigma ccl) with
-    | Prod (_,t,u) when is_empty_type u ->
+    match EConstr.kind sigma (hnf_constr env sigma ccl) with
+    | Prod (_,t,u) when is_empty_type sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
@@ -1082,7 +1099,7 @@ let find_sigma_data env s = build_sigma_type ()
  *)
 
 let make_tuple env sigma (rterm,rty) lind =
-  assert (dependent (mkRel lind) rty);
+  assert (not (noccurn sigma lind rty));
   let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
   let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
@@ -1092,6 +1109,8 @@ let make_tuple env sigma (rterm,rty) lind =
   let p = mkLambda (na, a, rty) in
   let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
   let sigma, sig_term = Evd.fresh_global env sigma sigdata.typ in
+  let exist_term = EConstr.of_constr exist_term in
+  let sig_term = EConstr.of_constr sig_term in
     sigma,
     (applist(exist_term,[a;p;(mkRel lind);rterm]),
      applist(sig_term,[a;p]))
@@ -1104,9 +1123,9 @@ let make_tuple env sigma (rterm,rty) lind =
    normalization *)
 
 let minimal_free_rels env sigma (c,cty) =
-  let cty_rels = free_rels cty in
+  let cty_rels = free_rels sigma cty in
   let cty' = simpl env sigma cty in
-  let rels' = free_rels cty' in
+  let rels' = free_rels sigma cty' in
   if Int.Set.subset cty_rels rels' then
     (cty,cty_rels)
   else
@@ -1174,19 +1193,18 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	error "Cannot solve a unification problem."
     else
       let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
-	| (_sigS,[a;p]) -> (a,p)
+	| (_sigS,[a;p]) -> (a, p)
  	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
       let ev = Evarutil.e_new_evar env evdref a in
-      let rty = beta_applist(p_i_minus_1,[ev]) in
+      let rty = beta_applist sigma (p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
-      match
-        Evd.existential_opt_value !evdref
-          (destEvar ev)
-      with
+      let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
+      match evopt with
 	| Some w ->
-            let w_type = unsafe_type_of env sigma w in
+            let w_type = unsafe_type_of env !evdref w in
             if Evarconv.e_cumul env evdref w_type a then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
+	      let exist_term = EConstr.of_constr exist_term in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
@@ -1267,7 +1285,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
   let sigma, (tuple,tuplety) =
     List.fold_left (fun (sigma, t) -> make_tuple env sigma t) (sigma, (z,zty)) sorted_rels
   in
-  assert (closed0 tuplety);
+  assert (closed0 sigma tuplety);
   let n = List.length sorted_rels in
   let sigma, dfltval = sig_clausal_form env sigma sort_of_zty n tuplety dflt in
     sigma, (tuple,tuplety,dfltval)
@@ -1287,56 +1305,46 @@ let build_injector env sigma dflt c cpath =
   let sigma, (injcode,resty,_) = build_injrec env sigma dflt c cpath in
     sigma, (injcode,resty)
 
-(*
-let try_delta_expand env sigma t =
-  let whdt = whd_all env sigma t  in
-  let rec hd_rec c  =
-    match kind_of_term c with
-      | Construct _ -> whdt
-      | App (f,_)  -> hd_rec f
-      | Cast (c,_,_) -> hd_rec c
-      | _  -> t
-  in
-  hd_rec whdt
-*)
-
 let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
 let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
 let inject_if_homogenous_dependent_pair ty =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   try
+    let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
     (* fetch the informations of the  pair *)
     let ceq = Universes.constr_of_global Coqlib.glob_eq in
+    let ceq = EConstr.of_constr ceq in
     let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
     let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
     (* check whether the equality deals with dep pairs or not *)
-    let eqTypeDest = fst (decompose_app t) in
-    if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit;
-    let hd1,ar1 = decompose_app_vect t1 and
-        hd2,ar2 = decompose_app_vect t2 in
-    if not (Globnames.is_global (existTconstr()) hd1) then raise Exit;
-    if not (Globnames.is_global (existTconstr()) hd2) then raise Exit;
-    let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
+    let eqTypeDest = fst (decompose_app sigma t) in
+    if not (Termops.is_global sigma (sigTconstr()) eqTypeDest) then raise Exit;
+    let hd1,ar1 = decompose_app_vect sigma t1 and
+        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
     (* 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 c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
+    let inj2 = EConstr.of_constr inj2 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;
        intro;
        onLastHyp (fun hyp ->
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
-          [clear [destVar hyp];
+          [clear [destVar sigma hyp];
            Proofview.V82.tactic (Tacmach.refine
              (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
           ])]
@@ -1350,7 +1358,7 @@ let inject_if_homogenous_dependent_pair ty =
 
 let simplify_args env sigma t =
   (* Quick hack to reduce in arguments of eq only *)
-  match decompose_app t with
+  match decompose_app sigma t with
     | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2])
     | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
     | _ -> t
@@ -1365,6 +1373,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in
       let injfun = mkNamedLambda e t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
+      let congr = EConstr.of_constr congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
       let sigma, pf_typ = Typing.type_of env sigma pf in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
@@ -1426,7 +1435,8 @@ let injEq ?(old=false) with_evars clear_flag ipats =
     match ipats_style with
     | Some ipats ->
       Proofview.Goal.enter { enter = begin fun gl ->
-        let destopt = match kind_of_term c with
+        let sigma = project gl in
+        let destopt = match EConstr.kind sigma c with
         | Var id -> get_previous_hyp_position id gl
         | _ -> MoveLast in
         let clear_tac =
@@ -1455,7 +1465,7 @@ let injConcl = injClause None false None
 let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
       match find_positions env sigma t1 t2 with
@@ -1476,9 +1486,9 @@ let dEq with_evars =
   dEqThen with_evars (fun clear_flag c x ->
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
-let intro_decomp_eq tac data cl =
+let intro_decomp_eq tac data (c, t) =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let cl = pf_apply make_clenv_binding gl cl NoBindings in
+    let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
     decompEqThen (fun _ -> tac) data cl
   end }
 
@@ -1516,14 +1526,14 @@ let _ = declare_intro_decomp_eq intro_decomp_eq
 
  *)
 
-let decomp_tuple_term env c t =
+let decomp_tuple_term env sigma c t =
   let rec decomprec inner_code ex exty =
     let iterated_decomp =
     try
-      let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose ex in
+      let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in
       let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
       and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
-      let cdrtyp = beta_applist (p,[car]) in
+      let cdrtyp = beta_applist sigma (p,[car]) in
       List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
     with Constr_matching.PatternMatchingFailure ->
       []
@@ -1534,8 +1544,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let sigma = Sigma.to_evar_map sigma in
   let typ = get_type_of env sigma dep_pair1 in
   (* We find all possible decompositions *)
-  let decomps1 = decomp_tuple_term env dep_pair1 typ in
-  let decomps2 = decomp_tuple_term env dep_pair2 typ in
+  let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
+  let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in
   (* We adjust to the shortest decomposition *)
   let n = min (List.length decomps1) (List.length decomps2) in
   let decomp1 = List.nth decomps1 (n-1) in
@@ -1547,10 +1557,10 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,subst_term e body)) e1_list b in
-  let pred_body = beta_applist(abst_B,proj_list) in
-  let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
-  let expected_goal = beta_applist (abst_B,List.map fst e2_list) in
+      (fun (e,t) body -> lambda_create env sigma (t,subst_term sigma e body)) e1_list b in
+  let pred_body = beta_applist sigma (abst_B,proj_list) in
+  let body = mkApp (lambda_create env sigma (typ,pred_body),[|dep_pair1|]) in
+  let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma expected_goal in
   (* Retype to get universes right *)
@@ -1564,7 +1574,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
@@ -1583,7 +1593,7 @@ let cutSubstInConcl l2r eqn =
   end }
 
 let cutSubstInHyp l2r eqn id =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
@@ -1672,14 +1682,14 @@ exception FoundHyp of (Id.t * constr * bool)
 let is_eq_x gl x d =
   let id = NamedDecl.get_id d in
   try
-    let is_var id c = match kind_of_term c with
+    let is_var id c = match EConstr.kind (project gl) c with
     | Var id' -> Id.equal id id'
     | _ -> false
     in
     let c = pf_nf_evar gl (NamedDecl.get_type d) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
-    if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true));
-    if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false))
+    if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true));
+    if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false))
   with Constr_matching.PatternMatchingFailure ->
     ()
 
@@ -1689,6 +1699,7 @@ let is_eq_x gl x d =
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
   Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
+  let sigma = Tacmach.New.project gl in
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   (* The set of hypotheses using x *)
@@ -1696,7 +1707,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
     List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) ->
       let id = NamedDecl.get_id dcl in
       if not (Id.equal id hyp)
-         && List.exists (fun y -> occur_var_in_decl env y dcl) deps
+         && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps
       then
         let id_dest = if !regular_subst_tactic then dest else MoveLast in
         (dest,id::deps,(id_dest,id)::allhyps)
@@ -1705,7 +1716,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
       hyps
       (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *)
   (* Decides if x appears in conclusion *)
-  let depconcl = occur_var env x concl in
+  let depconcl = occur_var env sigma x concl in
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
@@ -1768,13 +1779,15 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let find_equations gl =
     let gl = Proofview.Goal.assume gl in
     let env = Proofview.Goal.env gl in
+    let sigma = project gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     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 kind_of_term x, kind_of_term y with
+        match EConstr.kind sigma x, EConstr.kind sigma y with
         | Var z, _  when not (is_evaluable env (EvalVarRef z)) ->
             Some (NamedDecl.get_id decl)
         | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
@@ -1791,22 +1804,23 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let process hyp =
     Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
+    let sigma = project gl in
     let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
     let _,_,(_,x,y) = find_eq_data_decompose c in
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-    if Term.eq_constr x y then Proofview.tclUNIT () else
-      match kind_of_term x, kind_of_term y with
-      | Var x', _ when not (occur_term x y) && not (is_evaluable env (EvalVarRef x')) ->
+    if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
+      match EConstr.kind sigma x, EConstr.kind sigma y with
+      | Var x', _ when not (occur_term sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
           subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
-      | _, Var y' when not (occur_term y x) && not (is_evaluable env (EvalVarRef y')) ->
+      | _, Var y' when not (occur_term sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
           subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
       | _ ->
           Proofview.tclUNIT ()
     end }
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let ids = find_equations gl in
     tclMAP process ids
   end }
@@ -1816,17 +1830,19 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 (* Old implementation, not able to manage configurations like a=b, a=t,
    or situations like "a = S b, b = S a", or also accidentally unfolding
    let-ins *)
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let sigma = project gl in
   let find_eq_data_decompose = find_eq_data_decompose gl in
   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 *)
-      if Term.eq_constr x y then failwith "caught";
-      match kind_of_term x with Var x -> x | _ ->
-      match kind_of_term y with Var y -> y | _ -> failwith "caught"
+      if EConstr.eq_constr sigma x y then failwith "caught";
+      match EConstr.kind sigma x with Var x -> x | _ ->
+      match EConstr.kind sigma y with Var y -> y | _ -> failwith "caught"
     with Constr_matching.PatternMatchingFailure -> failwith "caught" in
   let test p = try Some (test p) with Failure _ -> None in
   let hyps = pf_hyps_types gl in
@@ -1870,7 +1886,7 @@ let rewrite_assumption_cond cond_eq_term cl =
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in
     let hyps = Proofview.Goal.hyps gl in
     arec hyps gl