Reductionops API using EConstr.

13 files changed, 93 insertions, 90 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index dae1cc9f1..46600cdd7 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -284,7 +284,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     match find_rel ctype with
     | Some c -> Some c
     | None ->
-	let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
+	let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *)
 	match find_rel (it_mkProd_or_LetIn t' ctx) with
 	| Some c -> Some c
 	| None -> None
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index fcbad4bf0..b9704b846 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -65,7 +65,7 @@ let contradiction_context =
       | d :: rest ->
           let id = NamedDecl.get_id d in
           let typ = nf_evar sigma (NamedDecl.get_type d) in
-	  let typ = whd_all env sigma typ in
+	  let typ = whd_all env sigma (EConstr.of_constr typ) in
 	  if is_empty_type sigma typ then
 	    simplest_elim (mkVar id)
 	  else match kind_of_term typ with
@@ -88,7 +88,7 @@ let contradiction_context =
 	      (Proofview.tclORELSE
                  (Proofview.Goal.enter { enter = begin fun gl ->
                    let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
-	           filter_hyp (fun typ -> is_conv_leq typ t)
+	           filter_hyp (fun typ -> is_conv_leq (EConstr.of_constr typ) (EConstr.of_constr t))
 		     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
                  end })
                  begin function (e, info) -> match e with
@@ -105,7 +105,7 @@ let is_negation_of env sigma typ t =
   match kind_of_term (whd_all env sigma t) with
     | Prod (na,t,u) ->
       let u = nf_evar sigma u in
-      is_empty_type sigma u && is_conv_leq env sigma typ t
+      is_empty_type sigma u && is_conv_leq env sigma (EConstr.of_constr typ) (EConstr.of_constr t)
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
@@ -114,7 +114,7 @@ let contradiction_term (c,lbind as cl) =
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let typ = type_of c in
-    let _, ccl = splay_prod env sigma typ in
+    let _, ccl = splay_prod env sigma (EConstr.of_constr typ) in
     if is_empty_type sigma ccl then
       Tacticals.New.tclTHEN
         (elim false None cl None)
@@ -123,7 +123,7 @@ let contradiction_term (c,lbind as cl) =
       Proofview.tclORELSE
         begin
           if lbind = NoBindings then
-            filter_hyp (is_negation_of env sigma typ)
+            filter_hyp (fun c -> is_negation_of env sigma typ (EConstr.of_constr c))
               (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
           else
             Proofview.tclZERO Not_found
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 6250fef2d..0869ac0c7 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -478,7 +478,7 @@ let unfold_head env (ids, csts) c =
 	true, Environ.constant_value_in env c
     | App (f, args) ->
 	(match aux f with
-	| true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args))
+	| true, f' -> true, Reductionops.whd_betaiota Evd.empty (EConstr.of_constr (mkApp (f', args)))
 	| false, _ -> 
 	    let done_, args' = 
 	      Array.fold_left_i (fun i (done_, acc) arg -> 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 12d8e98c4..b830ccefe 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -96,14 +96,14 @@ let head_in indl t gl =
     let ity,_ =
       if !up_to_delta
       then find_mrectype env sigma t
-      else extract_mrectype t
+      else extract_mrectype sigma t
     in List.exists (fun i -> eq_ind (fst i) (fst ity)) indl
   with Not_found -> false
 
 let decompose_these c l =
   Proofview.Goal.enter { enter = begin fun gl ->
   let indl = List.map (fun x -> x, Univ.Instance.empty) l in
-  general_decompose (fun sigma (_,t) -> head_in indl t gl) c
+  general_decompose (fun sigma (_,t) -> head_in indl (EConstr.of_constr t) gl) c
   end }
 
 let decompose_and c =
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 1a67bedc2..1554d43f0 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -197,7 +197,7 @@ let decideGralEquality =
       Proofview.Goal.enter { enter = begin fun gl ->
         let concl = pf_nf_concl gl in
         match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) ->
-        let headtyp = hd_app (pf_compute gl typ) in
+        let headtyp = hd_app (pf_compute gl (EConstr.of_constr typ)) in
         begin match kind_of_term headtyp with
         | Ind (mi,_) -> Proofview.tclUNIT mi
         | _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.")
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index c94dcfa9d..aea3ca17e 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -606,8 +606,8 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
 	  (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
 	    (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
 	      (Reductionops.whd_beta Evd.empty
-		(applist (c,
-	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
+		(EConstr.of_constr (applist (c,
+	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))
       in c', ctx'
   | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 74f6dd44a..48f46b36b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -328,7 +328,7 @@ let jmeq_same_dom gl = function
   | 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
+    match EConstr.decompose_app (project gl) (EConstr.of_constr t) with
       | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
       | _ -> false
 
@@ -402,7 +402,7 @@ let type_of_clause cls gl = match cls with
 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 ->
   let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
-  let isatomic = isProd (whd_zeta evd hdcncl) in
+  let isatomic = isProd (whd_zeta evd (EConstr.of_constr 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 evd (EConstr.of_constr c) (EConstr.of_constr type_of_cls) in
@@ -441,7 +441,7 @@ 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
+    let rels, t = decompose_prod_assum (whd_betaiotazeta sigma (EConstr.of_constr 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
@@ -457,7 +457,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
               | (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 *)
+	          let rels',t' = splay_prod_assum env' sigma (EConstr.of_constr t) in (* Search for underlying eq *)
 	          match match_with_equality_type sigma t' with
 	            | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -714,9 +714,11 @@ 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 open EConstr in
   let project env sorts posn t1 t2 =
+    let t1 = EConstr.Unsafe.to_constr t1 in
+    let t2 = EConstr.Unsafe.to_constr t2 in
     let ty1 = get_type_of env sigma t1 in
     let s = get_sort_family_of env sigma ty1 in
     if Sorts.List.mem s sorts
@@ -725,7 +727,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 (sp1,_), Construct (sp2,_)
           when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
             ->
@@ -760,7 +762,7 @@ let find_positions env sigma t1 t2 =
     let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
 		else [InSet;InType]
     in
-    Inr (findrec sorts [] t1 t2)
+    Inr (findrec sorts [] (EConstr.of_constr t1) (EConstr.of_constr t2))
   with DiscrFound (path,c1,c2) ->
     Inl (path,c1,c2)
 
@@ -840,7 +842,7 @@ let injectable env sigma t1 t2 =
 
 let descend_then env sigma head dirn =
   let IndType (indf,_) =
-    try find_rectype env sigma (get_type_of env sigma head)
+    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head))
     with Not_found ->
       error "Cannot project on an inductive type derived from a dependency." in
   let indp,_ = (dest_ind_family indf) in
@@ -883,7 +885,7 @@ let descend_then env sigma head dirn =
 
 let build_selector env sigma dirn c ind special default =
   let IndType(indf,_) =
-    try find_rectype env sigma ind
+    try find_rectype env sigma (EConstr.of_constr ind)
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors
           like T := c : (A:Set)A->T and a discrimination
@@ -1026,7 +1028,7 @@ let onNegatedEquality with_evars tac =
     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
+    match kind_of_term (hnf_constr env sigma (EConstr.of_constr ccl)) with
     | Prod (_,t,u) when is_empty_type sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
@@ -1104,7 +1106,7 @@ let make_tuple env sigma (rterm,rty) lind =
 
 let minimal_free_rels env sigma (c,cty) =
   let cty_rels = free_rels sigma (EConstr.of_constr cty) in
-  let cty' = simpl env sigma cty in
+  let cty' = simpl env sigma (EConstr.of_constr cty) in
   let rels' = free_rels sigma (EConstr.of_constr cty') in
   if Int.Set.subset cty_rels rels' then
     (cty,cty_rels)
@@ -1171,11 +1173,11 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       with Evarconv.UnableToUnify _ ->
 	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)
+      let (a,p_i_minus_1) = match whd_beta_stack !evdref (EConstr.of_constr p_i) with
+	| (_sigS,[a;p]) -> (EConstr.Unsafe.to_constr a, EConstr.Unsafe.to_constr 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 (EConstr.of_constr p_i_minus_1,[EConstr.of_constr ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
         Evd.existential_opt_value !evdref
@@ -1317,13 +1319,13 @@ let inject_if_homogenous_dependent_pair ty =
         hd2,ar2 = decompose_app_vect sigma (EConstr.of_constr 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 ind,_ = try pf_apply find_mrectype gl (EConstr.of_constr 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) &&
-      pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
+      pf_apply is_conv gl (EConstr.of_constr ar1.(2)) (EConstr.of_constr 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"
@@ -1350,8 +1352,8 @@ 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
-    | 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])
+    | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma (EConstr.of_constr c1);simpl env sigma (EConstr.of_constr c2)])
+    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma (EConstr.of_constr c1);t2;simpl env sigma (EConstr.of_constr c2)])
     | _ -> t
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
@@ -1515,14 +1517,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 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 (EConstr.of_constr p,[EConstr.of_constr car]) in
       List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
     with Constr_matching.PatternMatchingFailure ->
       []
@@ -1533,8 +1535,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,11 +1549,11 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let abst_B =
     List.fold_right
       (fun (e,t) body -> lambda_create env (t,subst_term sigma (EConstr.of_constr e) (EConstr.of_constr body))) e1_list b in
-  let pred_body = beta_applist(abst_B,proj_list) in
+  let pred_body = beta_applist sigma (EConstr.of_constr abst_B, List.map EConstr.of_constr 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
+  let expected_goal = beta_applist sigma (EConstr.of_constr abst_B,List.map (fst %> EConstr.of_constr) e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
-  let expected_goal = nf_betaiota sigma expected_goal in
+  let expected_goal = nf_betaiota sigma (EConstr.of_constr expected_goal) in
   (* Retype to get universes right *)
   let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
   let sigma, _ = Typing.type_of env sigma body in
@@ -1842,20 +1844,20 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 let cond_eq_term_left c t gl =
   try
     let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl c x then true else failwith "not convertible"
+    if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then true else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
     let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl c x then false else failwith "not convertible"
+    if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then false else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
     let (_,x,y) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl c x then true
-    else if pf_conv_x gl c y then false
+    if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then true
+    else if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr y) then false
     else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 55bf5f29e..c41f88ab7 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -761,7 +761,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
-  let cty = if hnf then hnf_constr env sigma cty else cty in
+  let cty = if hnf then hnf_constr env sigma (EConstr.of_constr cty) else cty in
     match kind_of_term cty with
     | Prod _ ->
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
@@ -910,7 +910,7 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
+  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
   let hd = head_of_constr_reference (head_constr sigma t) in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 847ecf4b0..a42a51fc0 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -440,7 +440,7 @@ let extract_eq_args gl = function
       let t = pf_unsafe_type_of gl e1 in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
-      if pf_conv_x gl t1 t2 then (t1,e1,e2)
+      if pf_conv_x gl (EConstr.of_constr t1) (EConstr.of_constr t2) then (t1,e1,e2)
       else raise PatternMatchingFailure
 
 let find_eq_data_decompose gl eqn =
@@ -466,7 +466,7 @@ let match_eq_nf gls eqn (ref, hetero) =
   match Id.Map.bindings (pf_matches gls pat eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
-	(t,pf_whd_all gls x,pf_whd_all gls y)
+	(t,pf_whd_all gls (EConstr.of_constr x),pf_whd_all gls (EConstr.of_constr y))
     | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
 
 let dest_nf_eq gls eqn =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index d1d6178da..0b2d2f0b2 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -443,7 +443,7 @@ let raw_inversion inv_kind id status names =
         let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
         CErrors.user_err  msg
     in
-    let IndType (indf,realargs) = find_rectype env sigma t in
+    let IndType (indf,realargs) = find_rectype env sigma (EConstr.of_constr t) in
     let evdref = ref sigma in
     let (elim_predicate, args) =
       make_inv_predicate env evdref indf realargs id status concl in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 46f1f7c8d..85910355e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -116,7 +116,7 @@ let max_prefix_sign lid sign =
     | id::l -> snd (max_rec (id, sign_prefix id sign) l)
 *)
 let rec add_prods_sign env sigma t =
-  match kind_of_term (whd_all env sigma t) with
+  match kind_of_term (whd_all env sigma (EConstr.of_constr t)) with
     | Prod (na,c1,b) ->
 	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
@@ -169,7 +169,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
       (pty,goal)
   in
-  let npty = nf_all env sigma pty in
+  let npty = nf_all env sigma (EConstr.of_constr pty) in
   let extenv = push_named (LocalAssum (p,npty)) env in
   extenv, goal
 
@@ -183,7 +183,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
 let inversion_scheme env sigma t sort dep_option inv_op =
   let (env,i) = add_prods_sign env sigma t in
   let ind =
-    try find_rectype env sigma i
+    try find_rectype env sigma (EConstr.of_constr i)
     with Not_found ->
       user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
   in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 15dd1a97c..c96553fae 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -502,7 +502,7 @@ let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast sigma
 | Prod (na, c1, b) ->
   if Int.equal k 1 then
     try
-      let ((sp, _), u), _ = find_inductive env sigma c1 in
+      let ((sp, _), u), _ = find_inductive env sigma (EConstr.of_constr c1) in
       (sp, u)
     with Not_found -> error "Cannot do a fixpoint on a non inductive type."
   else
@@ -555,14 +555,14 @@ let fix ido n = match ido with
     mutual_fix id n [] 0
 
 let rec check_is_mutcoind env sigma cl =
-  let b = whd_all env sigma cl in
+  let b = whd_all env sigma (EConstr.of_constr cl) in
   match kind_of_term b with
   | Prod (na, c1, b) ->
     let open Context.Rel.Declaration in
     check_is_mutcoind (push_rel (LocalAssum (na,c1)) env) sigma b
   | _ ->
     try
-      let _ = find_coinductive env sigma b in ()
+      let _ = find_coinductive env sigma (EConstr.of_constr b) in ()
     with Not_found ->
       error "All methods must construct elements in coinductive types."
 
@@ -609,11 +609,11 @@ let cofix ido = match ido with
 (*          Reduction and conversion tactics                  *)
 (**************************************************************)
 
-type tactic_reduction = env -> evar_map -> constr -> constr
+type tactic_reduction = env -> evar_map -> EConstr.t -> constr
 
 let pf_reduce_decl redfun where decl gl =
   let open Context.Named.Declaration in
-  let redfun' = Tacmach.New.pf_apply redfun gl in
+  let redfun' c = Tacmach.New.pf_apply redfun gl (EConstr.of_constr c) in
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
@@ -694,7 +694,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
 
 let reduct_in_concl (redfun,sty) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-    convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
+    convert_concl_no_check (Tacmach.New.pf_apply redfun gl (EConstr.of_constr (Tacmach.New.pf_concl gl))) sty
   end }
 
 let reduct_in_hyp ?(check=false) redfun (id,where) =
@@ -714,7 +714,7 @@ let reduct_option ?(check=false) redfun = function
 let pf_e_reduce_decl redfun where decl gl =
   let open Context.Named.Declaration in
   let sigma = Proofview.Goal.sigma gl in
-  let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma c in
+  let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (EConstr.of_constr c) in
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
@@ -729,7 +729,7 @@ let pf_e_reduce_decl redfun where decl gl =
 let e_reduct_in_concl ~check (redfun, sty) =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
+    let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (EConstr.of_constr (Tacmach.New.pf_concl gl)) in
     Sigma (convert_concl ~check c' sty, sigma, p)
   end }
 
@@ -749,7 +749,7 @@ let e_reduct_option ?(check=false) redfun = function
 let e_change_in_concl (redfun,sty) =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in
+    let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (EConstr.of_constr (Proofview.Goal.raw_concl gl)) in
     Sigma (convert_concl_no_check c sty, sigma, p)
   end }
 
@@ -759,14 +759,14 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
 	user_err  (pr_id id ++ str " has no value.");
-    let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in
+    let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma (EConstr.of_constr ty) in
     Sigma (LocalAssum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
       let Sigma (b', sigma, p) =
-	if where != InHypTypeOnly then (redfun true).e_redfun env sigma b else Sigma.here b sigma
+	if where != InHypTypeOnly then (redfun true).e_redfun env sigma (EConstr.of_constr b) else Sigma.here b sigma
       in
       let Sigma (ty', sigma, q) =
-	if where != InHypValueOnly then (redfun false).e_redfun env sigma ty else Sigma.here ty sigma
+	if where != InHypValueOnly then (redfun false).e_redfun env sigma (EConstr.of_constr ty) else Sigma.here ty sigma
       in
       Sigma (LocalDef (id,b',ty'), sigma, p +> q)
 
@@ -792,20 +792,21 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
     let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
     if not b then
       if
-        isSort (whd_all env sigma t1) &&
-        isSort (whd_all env sigma t2)
+        isSort (whd_all env sigma (EConstr.of_constr t1)) &&
+        isSort (whd_all env sigma (EConstr.of_constr t2))
       then (mayneedglobalcheck := true; sigma)
       else
         user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
     else sigma
   end
   else
-    if not (isSort (whd_all env sigma t1)) then
+    if not (isSort (whd_all env sigma (EConstr.of_constr t1))) then
       user_err ~hdr:"convert-check-hyp" (str "Not a type.")
     else sigma
 
 (* Now we introduce different instances of the previous tacticals *)
 let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun env sigma c ->
+  let c = EConstr.Unsafe.to_constr c in
   let Sigma (t', sigma, p) = t.run sigma in
   let sigma = Sigma.to_evar_map sigma in
   let sigma = check_types env sigma mayneedglobalcheck deep t' c in
@@ -1079,7 +1080,7 @@ let lookup_hypothesis_as_renamed_gen red h gl =
     match lookup_hypothesis_as_renamed env ccl h with
       | None when red ->
         let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in
-        let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in
+        let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) (EConstr.of_constr ccl) in
         aux c
       | x -> x
   in
@@ -1228,7 +1229,7 @@ let cut c =
       try
         (** Backward compat: ensure that [c] is well-typed. *)
         let typ = Typing.unsafe_type_of env sigma c in
-        let typ = whd_all env sigma typ in
+        let typ = whd_all env sigma (EConstr.of_constr typ) in
         match kind_of_term typ with
         | Sort _ -> true
         | _ -> false
@@ -1237,7 +1238,7 @@ let cut c =
     if is_sort then
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
       (** Backward compat: normalize [c]. *)
-      let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
+      let c = if normalize_cut then local_strong whd_betaiota sigma (EConstr.of_constr c) else c in
       Refine.refine ~unsafe:true { run = begin fun h ->
         let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
         let Sigma (x, h, q) = Evarutil.new_evar env h c in
@@ -1591,12 +1592,12 @@ let make_projection env sigma params cstr sign elim i n c u =
 	noccur_between 1 (n-i-1) t
 	(* to avoid surprising unifications, excludes flexible
 	projection types or lambda which will be instantiated by Meta/Evar *)
-	&& not (isEvar (fst (whd_betaiota_stack sigma t)))
+	&& not (EConstr.isEvar sigma (fst (whd_betaiota_stack sigma (EConstr.of_constr t))))
 	&& (accept_universal_lemma_under_conjunctions () || not (isRel t))
       then
         let t = lift (i+1-n) t in
-	let abselim = beta_applist (elim,params@[t;branch]) in
-	let c = beta_applist (abselim, [mkApp (c, Context.Rel.to_extended_vect 0 sign)]) in
+	let abselim = beta_applist sigma (EConstr.of_constr elim, List.map EConstr.of_constr (params@[t;branch])) in
+	let c = beta_applist sigma (EConstr.of_constr abselim, [EConstr.of_constr (mkApp (c, Context.Rel.to_extended_vect 0 sign))]) in
 	  Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
       else
 	None
@@ -1630,7 +1631,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
     | Some (_,_,isrec) ->
 	let n = (constructors_nrealargs ind).(0) in
 	let sort = Tacticals.New.elimination_sort_of_goal gl in
-	let IndType (indf,_) = find_rectype env sigma ccl in
+	let IndType (indf,_) = find_rectype env sigma (EConstr.of_constr ccl) in
 	let (_,inst), params = dest_ind_family indf in
 	let cstr = (get_constructors env indf).(0) in
 	let elim =
@@ -1703,7 +1704,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
 
-    let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in
+    let thm_ty0 = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma c)) in
     let try_apply thm_ty nprod =
       try
         let n = nb_prod_modulo_zeta sigma (EConstr.of_constr thm_ty) - nprod in
@@ -1716,7 +1717,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
     let rec try_red_apply thm_ty (exn0, info) =
       try
         (* Try to head-reduce the conclusion of the theorem *)
-        let red_thm = try_red_product env sigma thm_ty in
+        let red_thm = try_red_product env sigma (EConstr.of_constr thm_ty) in
         tclORELSEOPT
           (try_apply red_thm concl_nprod)
           (function (e, info) -> match e with
@@ -1829,7 +1830,7 @@ let progress_with_clause flags innerclause clause =
   with Not_found -> error "Unable to unify."
 
 let apply_in_once_main flags innerclause env sigma (d,lbind) =
-  let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in
+  let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma d)) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when CErrors.noncritical e ->
@@ -2127,7 +2128,7 @@ let apply_type newcl args =
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
     Refine.refine { run = begin fun sigma ->
-      let newcl = nf_betaiota (Sigma.to_evar_map sigma) newcl (* As in former Logic.refine *) in
+      let newcl = nf_betaiota (Sigma.to_evar_map sigma) (EConstr.of_constr newcl) (* As in former Logic.refine *) in
       let Sigma (ev, sigma, p) =
         Evarutil.new_evar env sigma ~principal:true ~store newcl in
       Sigma (applist (ev, args), sigma, p)
@@ -2318,7 +2319,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
     let sigma = Tacmach.New.project gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let whd_all = Tacmach.New.pf_apply whd_all gl in
-    let t = whd_all (type_of (mkVar id)) in
+    let t = whd_all (EConstr.of_constr (type_of (mkVar id))) in
     let eqtac, thin = match match_with_equality_type sigma t with
     | Some (hdcncl,[_;lhs;rhs]) ->
         if l2r && isVar lhs && not (occur_var env sigma (destVar lhs) (EConstr.of_constr rhs)) then
@@ -2905,13 +2906,13 @@ let specialize (c,lbind) ipat =
       let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
-      let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
+      let (thd,tstack) = whd_nored_stack clause.evd (EConstr.of_constr (clenv_value clause)) in
       let rec chk = function
       | [] -> []
-      | t::l -> if occur_meta clause.evd (EConstr.of_constr t) then [] else t :: chk l
+      | t::l -> if occur_meta clause.evd t then [] else EConstr.Unsafe.to_constr t :: chk l
       in
       let tstack = chk tstack in
-      let term = applist(thd,List.map (nf_evar clause.evd) tstack) in
+      let term = applist(EConstr.Unsafe.to_constr thd,List.map (nf_evar clause.evd) tstack) in
       if occur_meta clause.evd (EConstr.of_constr term) then
 	user_err  (str "Cannot infer an instance for " ++
 
@@ -2964,7 +2965,7 @@ let unfold_body x =
   in
   Tacticals.New.afterHyp x begin fun aft ->
   let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in
-  let rfun _ _ c = replace_vars [x, xval] c in
+  let rfun _ _ c = replace_vars [x, xval] (EConstr.Unsafe.to_constr c) in
   let reducth h = reduct_in_hyp rfun h in
   let reductc = reduct_in_concl (rfun, DEFAULTcast) in
   Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
@@ -3519,7 +3520,7 @@ let decompose_indapp f args =
 
 let mk_term_eq env sigma ty t ty' t' =
   let sigma = Sigma.to_evar_map sigma in
-  if Reductionops.is_conv env sigma ty ty' then
+  if Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty') then
     mkEq ty t t', mkRefl ty' t'
   else
     mkHEq ty t ty' t', mkHRefl ty' t'
@@ -3615,7 +3616,7 @@ let abstract_args gl generalize_vars dep id defined f args =
     *)
   let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg =
     let name, ty, arity =
-      let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
+      let rel, c = Reductionops.splay_prod_n env !sigma 1 (EConstr.of_constr prod) in
       let decl = List.hd rel in
       RelDecl.get_name decl, RelDecl.get_type decl, c
     in
@@ -3765,8 +3766,8 @@ let specialize_eqs id gl =
   in
   let ty' = it_mkProd_or_LetIn ty ctx'' in
   let acc' = it_mkLambda_or_LetIn acc ctx'' in
-  let ty' = Tacred.whd_simpl env !evars ty'
-  and acc' = Tacred.whd_simpl env !evars acc' in
+  let ty' = Tacred.whd_simpl env !evars (EConstr.of_constr ty')
+  and acc' = Tacred.whd_simpl env !evars (EConstr.of_constr acc') in
   let ty' = Evarutil.nf_evar !evars ty' in
     if worked then
       tclTHENFIRST (Tacmach.internal_cut true id ty')
@@ -4244,7 +4245,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
          known only by pattern-matching, as in the case of a term of
          the form "nat_rect ?A ?o ?s n", with ?A to be inferred by
          matching. *)
-      let sign,t = splay_prod env sigma typ in it_mkProd t sign
+      let sign,t = splay_prod env sigma (EConstr.of_constr typ) in it_mkProd t sign
     else
       (* Otherwise, we exclude the case of an induction argument in an
          explicitly functional type. Henceforth, we can complete the
@@ -4261,14 +4262,14 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
       let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in
       Sigma.Unsafe.of_pair (c, sigma)
     with e when catchable_exception e ->
-    try find_clause (try_red_product env sigma typ)
+    try find_clause (try_red_product env sigma (EConstr.of_constr typ))
     with Redelimination -> raise e in
   find_clause typ
 
 let check_expected_type env sigma (elimc,bl) elimt =
   (* Compute the expected template type of the term in case a using
      clause is given *)
-  let sign,_ = splay_prod env sigma elimt in
+  let sign,_ = splay_prod env sigma (EConstr.of_constr elimt) in
   let n = List.length sign in
   if n == 0 then error "Scheme cannot be applied.";
   let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
@@ -4283,7 +4284,7 @@ let check_enough_applied env sigma elim =
   | None ->
       (* No eliminator given *)
       fun u ->
-      let t,_ = decompose_app (whd_all env sigma u) in isInd t
+      let t,_ = decompose_app (whd_all env sigma (EConstr.of_constr u)) in isInd t
   | Some elimc ->
       let elimt = Retyping.get_type_of env sigma (fst elimc) in
       let scheme = compute_elim_sig ~elimc elimt in
@@ -4604,7 +4605,7 @@ let maybe_betadeltaiota_concl allowred gl =
   if not allowred then concl
   else
     let env = Proofview.Goal.env gl in
-    whd_all env sigma concl
+    whd_all env sigma (EConstr.of_constr concl)
 
 let reflexivity_red allowred =
   Proofview.Goal.enter { enter = begin fun gl ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7acfb6286..268453152 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -128,7 +128,7 @@ val exact_proof      : Constrexpr.constr_expr -> unit Proofview.tactic
 
 (** {6 Reduction tactics. } *)
 
-type tactic_reduction = env -> evar_map -> constr -> constr
+type tactic_reduction = env -> evar_map -> EConstr.t -> constr
 
 type change_arg = patvar_map -> constr Sigma.run