Eliminating parts of the right-hand side compatibility layer

5 files changed, 5 insertions, 21 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 0ca6615575..6c45bef1c6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1496,7 +1496,6 @@ let _ =
 
 let rec head_of_constr sigma t =
   let t = strip_outer_cast sigma (EConstr.of_constr (collapse_appl sigma t)) in
-  let t = EConstr.of_constr t in
     match EConstr.kind sigma t with
     | Prod (_,_,c2)  -> head_of_constr sigma c2
     | LetIn (_,_,_,c2) -> head_of_constr sigma c2
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4c79a61999..2eead2d22b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -183,7 +183,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
   let occs =
     w_unify_to_subterm_all ~flags env eqclause.evd
-      (EConstr.of_constr (if l2r then c1 else c2),EConstr.of_constr concl)
+      ((if l2r then c1 else c2),concl)
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
@@ -314,6 +314,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
     | None -> pf_nf_concl gl
     | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
     in
+    let typ = EConstr.of_constr typ in
     let cs = instantiate_lemma typ in
     if firstonly then tclFIRST (List.map try_clause cs)
     else tclMAP try_clause cs
@@ -1207,7 +1208,6 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
  	| _ -> 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 sigma (p_i_minus_1,[ev]) in
-      let rty = EConstr.of_constr rty in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
       match evopt with
@@ -1348,10 +1348,6 @@ let inject_if_homogenous_dependent_pair ty =
     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
-    let hd1 = EConstr.of_constr hd1 in
-    let hd2 = EConstr.of_constr hd2 in
-    let ar1 = Array.map EConstr.of_constr ar1 in
-    let ar2 = Array.map EConstr.of_constr ar2 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
@@ -1565,7 +1561,6 @@ let decomp_tuple_term env sigma c t =
       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 sigma (p,[car]) in
-      let cdrtyp = EConstr.of_constr cdrtyp in
       List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
     with Constr_matching.PatternMatchingFailure ->
       []
@@ -1593,13 +1588,11 @@ 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,EConstr.of_constr (subst_term sigma e body))) e1_list b in
+      (fun (e,t) body -> lambda_create env (t,subst_term sigma e body)) e1_list b in
   let pred_body = beta_applist sigma (abst_B,proj_list) in
-  let pred_body = EConstr.of_constr pred_body in
   let body = mkApp (lambda_create env (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 = EConstr.of_constr expected_goal in
   let expected_goal = nf_betaiota sigma expected_goal in
   let expected_goal = EConstr.of_constr expected_goal in
   (* Retype to get universes right *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index cd5fc79f5e..2b310033c3 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -50,7 +50,6 @@ exception Bound
 
 let head_constr_bound sigma t =
   let t = strip_outer_cast sigma t in
-  let t = EConstr.of_constr t in
   let _,ccl = decompose_prod_assum sigma t in
   let hd,args = decompose_app sigma ccl in
   match EConstr.kind sigma hd with
@@ -66,11 +65,8 @@ let head_constr sigma c =
 
 let decompose_app_bound sigma t =
   let t = strip_outer_cast sigma t in
-  let t = EConstr.of_constr t in
   let _,ccl = decompose_prod_assum sigma t in
   let hd,args = decompose_app_vect sigma ccl in
-  let hd = EConstr.of_constr hd in
-  let args = Array.map EConstr.of_constr args in
   match EConstr.kind sigma hd with
     | Const (c,u) -> ConstRef c, args
     | Ind (i,u) -> IndRef i, args
@@ -754,7 +750,6 @@ let secvars_of_global env gr =
 let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env sigma c in
   let cty = strip_outer_cast sigma cty in
-  let cty = EConstr.of_constr cty in
     match EConstr.kind sigma cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5c296b343f..ac9a564e58 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -462,7 +462,6 @@ let raw_inversion inv_kind id status names =
         Reductionops.beta_applist sigma (elim_predicate, realargs),
         case_nodep_then_using
     in
-    let cut_concl = EConstr.of_constr cut_concl in
     let refined id =
       let prf = mkApp (mkVar id, args) in
       Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 606eb27b9a..03f81773b1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -528,7 +528,7 @@ fun env sigma p -> function
   let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in
   Sigma (arg :: rem, sigma, r)
 
-let rec check_mutind env sigma k cl = match EConstr.kind sigma (EConstr.of_constr (strip_outer_cast sigma cl)) with
+let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast sigma cl) with
 | Prod (na, c1, b) ->
   if Int.equal k 1 then
     try
@@ -1647,10 +1647,8 @@ let make_projection env sigma params cstr sign elim i n c u =
       then
         let t = lift (i+1-n) t in
 	let abselim = beta_applist sigma (elim, params@[t;branch]) in
-	let abselim = EConstr.of_constr abselim in
 	let args = Array.map EConstr.of_constr (Context.Rel.to_extended_vect 0 sign) in
 	let c = beta_applist sigma (abselim, [mkApp (c, args)]) in
-	let c = EConstr.of_constr c in
 	  Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
       else
 	None
@@ -2856,7 +2854,7 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   let open Context.Rel.Declaration in
   let decls,cl = decompose_prod_n_assum sigma i cl in
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
-  let newdecls,_ = decompose_prod_n_assum sigma i (EConstr.of_constr (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod)) in
+  let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
   let cl' = EConstr.of_constr cl' in
   let na = generalized_name sigma c t ids cl' na in