Removing compatibility layers in Retyping

6 files changed, 11 insertions, 42 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b1d5d8135..2f8af6b44 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -283,7 +283,6 @@ let clenv_of_prods poly nprods (c, clenv) gl =
   else
     let sigma = Tacmach.New.project gl in
     let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
-    let ty = EConstr.of_constr ty in
     let diff = nb_prod sigma ty - nprods in
     if Pervasives.(>=) diff 0 then
       (* Was Some clenv... *)
@@ -477,7 +476,6 @@ let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
 
 let is_Prop env sigma concl =
   let ty = Retyping.get_type_of env sigma concl in
-  let ty = EConstr.of_constr ty in
   match EConstr.kind sigma ty with
   | Sort (Prop Null) -> true
   | _ -> false
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index e68267584..855273d3b 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -597,6 +597,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
 
 let fix_r2l_forward_rew_scheme (c, ctx') =
   let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) in
+  let t = EConstr.Unsafe.to_constr t in
   let ctx,_ = decompose_prod_assum t in
   match ctx with
   | hp :: p :: ind :: indargs ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 494f36d7d..e1c39bb34 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -188,7 +188,6 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
 
 let instantiate_lemma gl c ty l l2r concl =
   let sigma, ct = pf_type_of gl c in
-  let ct = EConstr.of_constr ct in
   let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
@@ -452,7 +451,6 @@ 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 ctype = EConstr.of_constr ctype in
     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 *)
@@ -635,8 +633,6 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   let get_type_of = pf_apply get_type_of gl in
   let t1 = get_type_of c1
   and t2 = get_type_of c2 in
-  let t1 = EConstr.of_constr t1 in
-  let t2 = EConstr.of_constr t2 in
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
@@ -733,7 +729,6 @@ let _ =
 let find_positions env sigma t1 t2 =
   let project env sorts posn t1 t2 =
     let ty1 = get_type_of env sigma t1 in
-    let ty1 = EConstr.of_constr ty1 in
     let s = get_sort_family_of env sigma ty1 in
     if Sorts.List.mem s sorts
     then [(List.rev posn,t1,t2)] else []
@@ -856,7 +851,7 @@ let injectable env sigma t1 t2 =
 
 let descend_then env sigma head dirn =
   let IndType (indf,_) =
-    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head))
+    try find_rectype env sigma (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
@@ -912,7 +907,6 @@ let build_selector env sigma dirn c ind special default =
   let (indp,_) = dest_ind_family indf in
   let ind, _ = check_privacy env indp in
   let typ = Retyping.get_type_of env sigma default in
-  let typ = EConstr.of_constr typ in
   let (mib,mip) = lookup_mind_specif env ind in
   let deparsign = make_arity_signature env true indf in
   let p = it_mkLambda_or_LetIn typ deparsign in
@@ -932,7 +926,6 @@ 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
-      let ind = EConstr.of_constr ind in
       let true_0,false_0 =
         build_coq_True(),build_coq_False() in
       build_selector env sigma dirn c ind true_0 false_0
@@ -1108,7 +1101,6 @@ let make_tuple env sigma (rterm,rty) lind =
   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 a = EConstr.of_constr a in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1396,7 +1388,6 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       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 pf_typ = EConstr.of_constr pf_typ in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
       let ty = simplify_args env sigma (clenv_type inj_clause) in
@@ -1567,7 +1558,6 @@ let lambda_create env (a,b) =
 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
-  let typ = EConstr.of_constr typ in
   (* We find all possible decompositions *)
   let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
   let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in
@@ -1659,7 +1649,6 @@ let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 let substClause l2r c cls =
   Proofview.Goal.enter { enter = begin fun gl ->
   let eq = pf_apply get_type_of gl c in
-  let eq = EConstr.of_constr eq in
   tclTHENS (cutSubstClause l2r eq cls)
     [Proofview.tclUNIT (); exact_no_check c]
   end }
diff --git a/tactics/hints.ml b/tactics/hints.ml
index d4b73706c..9e9635e8a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -855,7 +855,6 @@ let fresh_global_or_constr env sigma poly cr =
 let make_resolves env sigma flags pri poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
   let cty = Retyping.get_type_of env sigma c in
-  let cty = EConstr.of_constr cty in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
diff --git a/tactics/inv.ml b/tactics/inv.ml
index e45eb2a16..a398e04dd 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -63,10 +63,10 @@ let var_occurs_in_pf gl id =
 
  *)
 
-type inversion_status = Dep of EConstr.constr option | NoDep
+type inversion_status = Dep of constr option | NoDep
 
 let compute_eqn env sigma n i ai =
-  (mkRel (n-i),EConstr.of_constr (get_type_of env sigma (mkRel (n-i))))
+  (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
 
 let make_inv_predicate env evd indf realargs id status concl =
   let nrealargs = List.length realargs in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b2f2797a6..574f1c6f3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -818,13 +818,10 @@ let make_change_arg c pats =
 
 let check_types env sigma mayneedglobalcheck deep newc origc =
   let t1 = Retyping.get_type_of env sigma newc in
-  let t1 = EConstr.of_constr t1 in
   if deep then begin
     let t2 = Retyping.get_type_of env sigma origc in
-    let t2 = EConstr.of_constr t2 in
     let sigma, t2 = Evarsolve.refresh_universes
 		      ~onlyalg:true (Some false) env sigma t2 in
-    let t2 = EConstr.of_constr t2 in
     let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
     if not b then
       if
@@ -1448,7 +1445,6 @@ let general_elim_clause_gen elimtac indclause elim =
   let sigma = Tacmach.New.project gl in
   let (elimc,lbindelimc) = elim.elimbody in
   let elimt = Retyping.get_type_of env sigma elimc in
-  let elimt = EConstr.of_constr elimt in
   let i =
     match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in
   elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
@@ -1459,7 +1455,6 @@ 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 c in
-  let ct = EConstr.of_constr ct in
   let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
   let elimtac = elimination_clause_scheme with_evars in
   let indclause  = make_clenv_binding env sigma (c, t) lbindc in
@@ -1478,7 +1473,6 @@ 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) 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) =
@@ -1598,7 +1592,6 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
   let hyp = mkVar id in
   let hyp_typ = Retyping.get_type_of env sigma hyp in
-  let hyp_typ = EConstr.of_constr hyp_typ in
   let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
   let new_hyp_typ  = clenv_type elimclause'' in
@@ -1662,7 +1655,6 @@ let make_projection env sigma params cstr sign elim i n c u =
 	  in
 	  let app = it_mkLambda_or_LetIn proj sign in
 	  let t = Retyping.get_type_of env sigma app in
-	  let t = EConstr.of_constr t in
 	    Some (app, t)
       | None -> None
   in elim
@@ -1673,7 +1665,6 @@ 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 c in
-    let t = EConstr.of_constr t in
     let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
     let sign,ccl = EConstr.decompose_prod_assum sigma t in
     match match_with_tuple sigma ccl with
@@ -1755,7 +1746,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 (EConstr.of_constr (Retyping.get_type_of env sigma c)) in
+    let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in
     let try_apply thm_ty nprod =
       try
         let n = nb_prod_modulo_zeta sigma thm_ty - nprod in
@@ -1881,7 +1872,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 (EConstr.of_constr (Retyping.get_type_of env sigma d)) in
+  let thm = nf_betaiota sigma (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 ->
@@ -1993,7 +1984,6 @@ let exact_check c =
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map sigma in
   let sigma, ct = Typing.type_of env sigma c in
-  let ct = EConstr.of_constr ct in
   let tac =
       Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c)
   in
@@ -2662,9 +2652,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
     | Some t -> Sigma.here t sigma
     | None ->
       let t = typ_of env sigma c in
-      let t = EConstr.of_constr t in
       let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in
-      let c = EConstr.of_constr c in
       Sigma.Unsafe.of_pair (c, sigma)
     in
     let Sigma ((newcl, eq_tac), sigma, q) = match with_eq with
@@ -2717,7 +2705,7 @@ let insert_before decls lasthyp env =
 
 let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
   let open Context.Named.Declaration in
-  let t = match ty with Some t -> t | _ -> EConstr.of_constr (typ_of env sigma c) in
+  let t = match ty with Some t -> t | _ -> typ_of env sigma c in
   let decl = if dep then nlocal_def (id,c,t)
 	     else nlocal_assum (id,t)
   in
@@ -2850,7 +2838,6 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
   let env = Tacmach.pf_env gl in
   let ids = Tacmach.pf_ids_of_hyps gl in
   let sigma, t = Typing.type_of env sigma c in
-  let t = EConstr.of_constr t in
   generalize_goal_gen env sigma ids i o t cl
 
 let old_generalize_dep ?(with_let=false) c gl =
@@ -2923,7 +2910,6 @@ let new_generalize_gen_let lconstr =
       List.fold_right_i 
 	(fun i ((_,c,b),_ as o) (cl, sigma, args) ->
 	  let sigma, t = Typing.type_of env sigma c in
-	  let t = EConstr.of_constr t in
 	  let args = if Option.is_empty b then c :: args else args in
           let cl, sigma = generalize_goal_gen env sigma ids i o t cl in
           (cl, sigma, args))
@@ -2974,7 +2960,7 @@ let specialize (c,lbind) ipat =
       let sigma = Typeclasses.resolve_typeclasses env sigma in
       sigma, nf_evar sigma c
     else
-      let clause = make_clenv_binding env sigma (c,EConstr.of_constr (Retyping.get_type_of env sigma c)) lbind in
+      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
@@ -2991,7 +2977,6 @@ let specialize (c,lbind) ipat =
 	  str ".");
       clause.evd, term in
   let typ = Retyping.get_type_of env sigma term in
-  let typ = EConstr.of_constr typ in
   let tac =
     match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with
     | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) ->
@@ -3699,7 +3684,6 @@ let abstract_args gl generalize_vars dep id defined f args =
     let argty = EConstr.of_constr argty in
     let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
     let () = sigma := sigma' in
-    let ty = EConstr.of_constr ty in
     let lenctx = List.length ctx in
     let liftargty = lift lenctx argty in
     let leq = constr_cmp !sigma Reduction.CUMUL liftargty ty in
@@ -3751,7 +3735,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 	else []
       in
       let body, c' =
-	if defined then Some c', EConstr.of_constr (Retyping.get_type_of ctxenv !sigma c')
+	if defined then Some c', Retyping.get_type_of ctxenv !sigma c'
 	else None, c'
       in
       let typ = Tacmach.pf_get_hyp_typ gl id in
@@ -4339,7 +4323,6 @@ let clear_unselected_context id inhyps cls =
 
 let use_bindings env sigma elim must_be_closed (c,lbind) typ =
   let sigma = Sigma.to_evar_map sigma in
-  let typ = EConstr.of_constr typ in
   let typ =
     if elim == None then
       (* w/o an scheme, the term has to be applied at least until
@@ -4389,7 +4372,6 @@ let check_enough_applied env sigma elim =
       let t,_ = decompose_app sigma (whd_all env sigma u) in isInd sigma t
   | Some elimc ->
       let elimt = Retyping.get_type_of env sigma (fst elimc) in
-      let elimt = EConstr.of_constr elimt in
       let scheme = compute_elim_sig sigma ~elimc elimt in
       match scheme.indref with
       | None ->
@@ -4435,7 +4417,6 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
           let b = not with_evars && with_eq != None in
           let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in
           let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
-          let t = EConstr.of_constr t in
           let Sigma (ans, sigma, q) = mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) in
           Sigma (ans, sigma, p +> q)
         end };
@@ -4487,7 +4468,7 @@ let induction_gen clear_flag isrec with_evars elim
     && lbind == NoBindings && not with_evars && Option.is_empty eqname
     && clear_flag == None
     && has_generic_occurrences_but_goal cls (destVar evd c) env evd ccl in
-  let enough_applied = check_enough_applied env sigma elim (EConstr.of_constr t) in
+  let enough_applied = check_enough_applied env sigma elim t in
   if is_arg_pure_hyp && enough_applied then
     (* First case: induction on a variable already in an inductive type and
        with maximal abstraction over the variable.
@@ -4504,6 +4485,7 @@ let induction_gen clear_flag isrec with_evars elim
      declaring the induction argument as a new local variable *)
     let id =
     (* Type not the right one if partially applied but anyway for internal use*)
+      let t = EConstr.Unsafe.to_constr t in
       let x = id_of_name_using_hdchar (Global.env()) t Anonymous in
       new_fresh_id [] x gl in
     let info_arg = (is_arg_pure_hyp, not enough_applied) in