Tacmach API using EConstr.

10 files changed, 51 insertions, 33 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b0f3551705..a2699ba8d9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -226,7 +226,7 @@ let e_give_exact flags poly (c,clenv) gl =
         c, {gl with sigma = evd}
     else c, gl
   in
-  let t1 = pf_unsafe_type_of gl c in
+  let t1 = pf_unsafe_type_of gl (EConstr.of_constr c) in
   Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
@@ -1514,7 +1514,7 @@ let is_ground c gl =
 let autoapply c i gl =
   let flags = auto_unif_flags Evar.Set.empty
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
-  let cty = pf_unsafe_type_of gl c in
+  let cty = pf_unsafe_type_of gl (EConstr.of_constr c) in
   let ce = mk_clenv_from gl (c,cty) in
   let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl
     ((c,cty,Univ.ContextSet.empty),0,ce) } in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9580fdbfca..2058b95a6a 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) =
     let sigma = Tacmach.New.project gl in
     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 typ = type_of (EConstr.of_constr c) in
     let _, ccl = splay_prod env sigma (EConstr.of_constr typ) in
     if is_empty_type sigma ccl then
       Tacticals.New.tclTHEN
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 0869ac0c76..2fad4fcf7f 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -30,7 +30,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let t1 = Tacmach.New.pf_unsafe_type_of gl c in
+  let t1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
   let sigma = Tacmach.New.project gl in
   if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then
diff --git a/tactics/elim.ml b/tactics/elim.ml
index b830ccefee..bcb1c05cc9 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -80,7 +80,7 @@ let general_decompose recognizer c =
   Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let sigma = project gl in
-  let typc = type_of c in
+  let typc = type_of (EConstr.of_constr c) in
   tclTHENS (cut typc)
     [ tclTHEN (intro_using tmphyp_name)
          (onLastHypId
@@ -133,7 +133,7 @@ let induction_trailer abs_i abs_j bargs =
     (onLastHypId
        (fun id ->
           Proofview.Goal.nf_enter { enter = begin fun gl ->
-	  let idty = pf_unsafe_type_of gl (mkVar id) in
+	  let idty = pf_unsafe_type_of gl (EConstr.mkVar id) in
 	  let fvty = global_vars (pf_env gl) (project gl) (EConstr.of_constr idty) in
 	  let possible_bring_hyps =
 	    (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 1554d43f09..d1b14a9076 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -156,7 +156,7 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
   ]
 | a1 :: largs, a2 :: rargs ->
   Proofview.Goal.enter { enter = begin fun gl ->
-  let rectype = pf_unsafe_type_of gl a1 in
+  let rectype = pf_unsafe_type_of gl (EConstr.of_constr a1) in
   let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
   let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
   let subtacs =
@@ -226,7 +226,7 @@ let decideEquality rectype =
 
 let compare c1 c2 =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let rectype = pf_unsafe_type_of gl c1 in
+  let rectype = pf_unsafe_type_of gl (EConstr.of_constr c1) in
   let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
   (tclTHENS (cut decide)
             [(tclTHEN  intro
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 64b56b99bc..ad80d2d1fb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -181,8 +181,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let sigma, ct = pf_type_of gl c in
-  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
+  let sigma, ct = pf_type_of gl (EConstr.of_constr c) in
+  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma (EConstr.of_constr ct)) with UserError _ -> ct in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
 
@@ -992,6 +992,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
+  let pf = EConstr.of_constr pf in
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
   tclTHENS (assert_after Anonymous absurd_term)
@@ -1012,8 +1013,8 @@ let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.nf_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
-  let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
+  let t = type_of (EConstr.of_constr c) in
+  let t' = try snd (reduce_to_quantified_ind (EConstr.of_constr t)) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
@@ -1327,7 +1328,7 @@ let inject_if_homogenous_dependent_pair ty =
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
       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 new_eq_args = [|pf_unsafe_type_of gl (EConstr.of_constr 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
@@ -1339,7 +1340,7 @@ let inject_if_homogenous_dependent_pair ty =
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar hyp];
            Proofview.V82.tactic (Tacmach.refine
-             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
+             (EConstr.of_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
           ])]
   with Exit ->
     Proofview.tclUNIT ()
@@ -1384,7 +1385,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       (Proofview.tclIGNORE (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
            [inject_if_homogenous_dependent_pair ty;
-            Proofview.V82.tactic (Tacmach.refine pf)])
+            Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 87e252a380..5d78fd5853 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -437,7 +437,7 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *)
 
 let extract_eq_args gl = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = pf_unsafe_type_of gl e1 in (t,e1,e2)
+      let t = pf_unsafe_type_of gl (EConstr.of_constr e1) in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
       if pf_conv_x gl (EConstr.of_constr t1) (EConstr.of_constr t2) then (t1,e1,e2)
@@ -463,6 +463,7 @@ let match_eq_nf gls eqn (ref, hetero) =
   let n = if hetero then 4 else 3 in
   let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in
   let pat = mkPattern (mkGAppRef ref args) in
+  let eqn = EConstr.of_constr eqn in
   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);
diff --git a/tactics/inv.ml b/tactics/inv.ml
index eebc672224..2f5186f81f 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -438,7 +438,7 @@ let raw_inversion inv_kind id status names =
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
     let (ind, t) =
-      try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
+      try pf_apply Tacred.reduce_to_atomic_ind gl (EConstr.of_constr (pf_unsafe_type_of gl (EConstr.of_constr c)))
       with UserError _ ->
         let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
         CErrors.user_err  msg
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 2754db0101..02909243d5 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -628,7 +628,7 @@ module New = struct
     (Proofview.Goal.nf_enter { enter = begin fun gl ->
     let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
     (* applying elimination_scheme just a little modified *)
-    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
+    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim))) gl in
     let indmv =
       match kind_of_term (last_arg elimclause.evd (EConstr.of_constr elimclause.templval.Evd.rebus)) with
       | Meta mv -> mv
@@ -678,7 +678,7 @@ module New = struct
 
   let elimination_then tac c =
     Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
+    let (ind,t) = pf_reduce_to_quantified_ind gl (EConstr.of_constr (pf_unsafe_type_of gl (EConstr.of_constr c))) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
       | None -> true,gl_make_elim
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 639a12b343..b9a219a2c9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -457,6 +457,7 @@ let assert_before_then_gen b naming t tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
     let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
+    let t = EConstr.of_constr t in
     Tacticals.New.tclTHENLAST
       (Proofview.V82.tactic
          (fun gl ->
@@ -476,6 +477,7 @@ let assert_after_then_gen b naming t tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
     let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
+    let t = EConstr.of_constr t in
     Tacticals.New.tclTHENFIRST
       (Proofview.V82.tactic
          (fun gl ->
@@ -1303,6 +1305,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
   if not with_evars && occur_meta clenv.evd (EConstr.of_constr new_hyp_typ) then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
+  let new_hyp_prf = EConstr.of_constr new_hyp_prf in
   let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in
   let naming = NamingMustBe (dloc,targetid) in
   let with_clear = do_replace (Some id) naming in
@@ -1434,7 +1437,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let ct = Retyping.get_type_of env sigma (EConstr.of_constr c) in
-  let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
+  let t = try snd (reduce_to_quantified_ind env sigma (EConstr.of_constr ct)) with UserError _ -> ct in
   let elimtac = elimination_clause_scheme with_evars in
   let indclause  = make_clenv_binding env sigma (c, t) lbindc in
   let sigma = meta_merge sigma (clear_metas indclause.evd) in
@@ -1452,6 +1455,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
   let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c) in
+  let t = EConstr.of_constr t 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 Sigma (elim, sigma, p) =
@@ -1491,7 +1495,8 @@ let find_ind_eliminator ind s gl =
     evd, c
 
 let find_eliminator c gl =
-  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
+  let c = EConstr.of_constr c in
+  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl c)) in
   if is_nonrec ind then raise IsNonrec;
   let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
     evd, {elimindex = None; elimbody = (c,NoBindings);
@@ -1637,6 +1642,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
   let sigma = Tacmach.New.project gl in
   try
     let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
+    let t = EConstr.of_constr t in
     let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
     let sign,ccl = decompose_prod_assum t in
     match match_with_tuple sigma ccl with
@@ -1661,6 +1667,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
 	    match make_projection env sigma params cstr sign elim i n c u with
 	    | None -> Tacticals.New.tclFAIL 0 (mt())
 	    | Some (p,pt) ->
+              let p = EConstr.of_constr p in
 	      Tacticals.New.tclTHENS
 		(assert_before_gen false (NamingAvoid avoid) pt)
 		[Proofview.V82.tactic (refine p);
@@ -1920,7 +1927,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
 let cut_and_apply c =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
-    match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
+    match kind_of_term (Tacmach.New.pf_hnf_constr gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c)))) with
       | Prod (_,c1,c2) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr c2) ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
@@ -2201,6 +2208,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
+    let cl = EConstr.of_constr cl in
     let (mind,redcl) = reduce_to_quantified_ind cl in
     let nconstr =
       Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
@@ -2240,6 +2248,7 @@ let any_constructor with_evars tacopt =
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
+    let cl = EConstr.of_constr cl in
     let mind = fst (reduce_to_quantified_ind cl) in
     let nconstr =
       Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
@@ -2298,7 +2307,8 @@ let my_find_eq_data_decompose gl t =
 let intro_decomp_eq loc l thin tac id =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_unsafe_type_of gl c in
+  let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
+  let t = EConstr.of_constr t in
   let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   match my_find_eq_data_decompose gl t with
   | Some (eq,u,eq_args) ->
@@ -2312,7 +2322,8 @@ let intro_decomp_eq loc l thin tac id =
 let intro_or_and_pattern loc with_evars bracketed ll thin tac id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_unsafe_type_of gl c in
+  let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
+  let t = EConstr.of_constr t in
   let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   let branchsigns = compute_constructor_signatures false ind in
   let nv_with_let = Array.map List.length branchsigns in
@@ -2337,7 +2348,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 (EConstr.of_constr (type_of (mkVar id))) in
+    let t = whd_all (EConstr.of_constr (type_of (EConstr.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
@@ -2747,7 +2758,7 @@ let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.enter { enter = begin fun gl ->
-      let t = Tacmach.New.pf_unsafe_type_of gl c in
+      let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
       let hd = head_ident c in
       Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
       end }
@@ -3233,7 +3244,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             | Var id -> id
             | _ ->
             let type_of = Tacmach.New.pf_unsafe_type_of gl in
-            id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+            id_of_name_using_hdchar (Global.env()) (type_of (EConstr.of_constr c)) Anonymous in
             let x = fresh_id_in_env avoid id env in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
@@ -3645,7 +3656,7 @@ let abstract_args gl generalize_vars dep id defined f args =
       let decl = List.hd rel in
       RelDecl.get_name decl, RelDecl.get_type decl, c
     in
-    let argty = Tacmach.pf_unsafe_type_of gl arg in
+    let argty = Tacmach.pf_unsafe_type_of gl (EConstr.of_constr arg) in
     let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma (EConstr.of_constr ty) in
     let () = sigma := sigma' in
     let lenctx = List.length ctx in
@@ -3686,7 +3697,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 	      true, mkApp (f', before), after
   in
     if dogen then
-      let tyf' = Tacmach.pf_unsafe_type_of gl f' in
+      let tyf' = Tacmach.pf_unsafe_type_of gl (EConstr.of_constr f') in
       let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
 	Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
       in
@@ -3794,6 +3805,7 @@ let specialize_eqs id gl =
   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
+  let ty' = EConstr.of_constr ty' in
     if worked then
       tclTHENFIRST (Tacmach.internal_cut true id ty')
 	(Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
@@ -4014,6 +4026,7 @@ 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 tmptyp0 = EConstr.of_constr tmptyp0 in
   let mind,_ = 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
@@ -4028,12 +4041,13 @@ let guess_elim isrec dep s hyp0 gl =
         let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma mind s in
         (Sigma.to_evar_map sigma, ind)
   in
-  let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
+  let elimt = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elimc) in
     evd, ((elimc, NoBindings), elimt), mkIndU mind
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in
+  let elimc = EConstr.of_constr elimc in
   Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
 
 type scheme_signature =
@@ -4069,7 +4083,7 @@ let get_elim_signature elim hyp0 gl =
   compute_elim_signature (given_elim hyp0 elim gl) hyp0
 
 let is_functional_induction elimc gl =
-  let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in
+  let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr (fst elimc))) in
   (* The test is not safe: with non-functional induction on non-standard
      induction scheme, this may fail *)
   Option.is_empty scheme.indarg
@@ -4466,7 +4480,7 @@ let induction_gen_l isrec with_evars elim names lc =
                 let type_of = Tacmach.New.pf_unsafe_type_of gl in
                 let sigma = Tacmach.New.project gl in
                 let x =
-		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+		  id_of_name_using_hdchar (Global.env()) (type_of (EConstr.of_constr c)) Anonymous in
 
                 let id = new_fresh_id [] x gl in
 		let newl' = List.map (fun r -> replace_term sigma (EConstr.of_constr c) (EConstr.mkVar id) (EConstr.of_constr r)) l' in
@@ -4606,6 +4620,7 @@ let elim_scheme_type elim t =
 
 let elim_type t =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let t = EConstr.of_constr t in
   let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
   let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in
   Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd)
@@ -4613,6 +4628,7 @@ let elim_type t =
 
 let case_type t =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let t = EConstr.of_constr t in
   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
@@ -4717,7 +4733,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
+  let ctype = Tacmach.New.pf_unsafe_type_of gl (EConstr.mkVar id) in
   let sign,t = decompose_prod_assum ctype in
   Proofview.tclORELSE
     begin