Retyping API using EConstr.

8 files changed, 45 insertions, 45 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index fe7a09f77d..6fb90e7af3 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -280,7 +280,7 @@ let clenv_of_prods poly nprods (c, clenv) gl =
   if poly || Int.equal nprods 0 then Some (None, clenv)
   else
     let sigma = Tacmach.New.project gl in
-    let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
+    let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma (EConstr.of_constr c) in
     let diff = nb_prod sigma (EConstr.of_constr ty) - nprods in
     if Pervasives.(>=) diff 0 then
       (* Was Some clenv... *)
@@ -473,7 +473,7 @@ let catchable = function
 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 = Retyping.get_type_of env sigma (EConstr.of_constr concl) in
   match kind_of_term ty with
   | Sort (Prop Null) -> true
   | _ -> false
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index b9704b846f..789028ac15 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -28,7 +28,7 @@ let absurd c =
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let sigma = Sigma.to_evar_map sigma in
-    let j = Retyping.get_judgment_of env sigma c in
+    let j = Retyping.get_judgment_of env sigma (EConstr.of_constr c) in
     let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
     let t = j.Environ.utj_val in
     let tac =
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index aea3ca17ec..92480e253b 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -596,7 +596,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 c in
+  let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) 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 48f46b36be..e87746a28e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -440,7 +440,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     Proofview.Goal.enter { enter = begin fun gl ->
       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 = get_type_of env sigma (EConstr.of_constr c) 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 *)
@@ -621,8 +621,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   in
   Proofview.Goal.enter { enter = begin fun gl ->
   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 = get_type_of (EConstr.of_constr c1)
+  and t2 = get_type_of (EConstr.of_constr c2) in
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
@@ -719,8 +719,8 @@ let find_positions env sigma t1 t2 =
   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
+    let ty1 = get_type_of env sigma (EConstr.of_constr t1) in
+    let s = get_sort_family_of env sigma (EConstr.of_constr ty1) in
     if Sorts.List.mem s sorts
     then [(List.rev posn,t1,t2)] else []
   in
@@ -842,7 +842,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 (EConstr.of_constr (get_type_of env sigma (EConstr.of_constr head)))
     with Not_found ->
       error "Cannot project on an inductive type derived from a dependency." in
   let indp,_ = (dest_ind_family indf) in
@@ -897,7 +897,7 @@ let build_selector env sigma dirn c ind special default =
 		 dependent types.") in
   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 = Retyping.get_type_of env sigma (EConstr.of_constr default) 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
@@ -912,7 +912,7 @@ let build_selector env sigma dirn c ind special default =
 
 let rec build_discriminator env sigma dirn c = function
   | [] ->
-      let ind = get_type_of env sigma c in
+      let ind = get_type_of env sigma (EConstr.of_constr c) in
       let true_0,false_0 =
         build_coq_True(),build_coq_False() in
       build_selector env sigma dirn c ind true_0 false_0
@@ -1084,7 +1084,7 @@ let find_sigma_data env s = build_sigma_type ()
 
 let make_tuple env sigma (rterm,rty) lind =
   assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
-  let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
+  let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr 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
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
@@ -1262,7 +1262,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 
 let make_iterated_tuple env sigma dflt (z,zty) =
   let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
-  let sort_of_zty = get_sort_of env sigma zty in
+  let sort_of_zty = get_sort_of env sigma (EConstr.of_constr zty) in
   let sorted_rels = Int.Set.elements rels in
   let sigma, (tuple,tuplety) =
     List.fold_left (fun (sigma, t) -> make_tuple env sigma t) (sigma, (z,zty)) sorted_rels
@@ -1533,7 +1533,7 @@ let decomp_tuple_term env sigma c t =
 
 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 = get_type_of env sigma (EConstr.of_constr dep_pair1) 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
@@ -1623,7 +1623,7 @@ 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 = pf_apply get_type_of gl (EConstr.of_constr c) in
   tclTHENS (cutSubstClause l2r eq cls)
     [Proofview.tclUNIT (); exact_no_check c]
   end }
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c41f88ab7f..2aa4347779 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -846,7 +846,7 @@ 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 = Retyping.get_type_of env sigma (EConstr.of_constr c) 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 0b2d2f0b2f..38f75995b9 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -65,7 +65,7 @@ let var_occurs_in_pf gl id =
 type inversion_status = Dep of constr option | NoDep
 
 let compute_eqn env sigma n i ai =
-  (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
+  (mkRel (n-i),get_type_of env sigma (EConstr.of_constr (mkRel (n-i))))
 
 let make_inv_predicate env evd indf realargs id status concl =
   let nrealargs = List.length realargs in
@@ -86,7 +86,7 @@ let make_inv_predicate env evd indf realargs id status concl =
             match dflt_concl with
               | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
               | None ->
-		let sort = get_sort_family_of env !evd concl in
+		let sort = get_sort_family_of env !evd (EConstr.of_constr concl) in
 		let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in
 		let p = make_arity env true indf sort in
 		let evd',(p,ptyp) = Unification.abstract_list_all env
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 676b23d095..2754db0101 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -248,10 +248,10 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
   Array.map2 analrec lc lrecargs
 
 let elimination_sort_of_goal gl =
-  pf_apply Retyping.get_sort_family_of gl (pf_concl gl)
+  pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr (pf_concl gl))
 
 let elimination_sort_of_hyp id gl =
-  pf_apply Retyping.get_sort_family_of gl (pf_get_hyp_typ gl id)
+  pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr (pf_get_hyp_typ gl id))
 
 let elimination_sort_of_clause = function
   | None -> elimination_sort_of_goal
@@ -708,12 +708,12 @@ module New = struct
   let elimination_sort_of_goal gl =
     (** Retyping will expand evars anyway. *)
     let c = Proofview.Goal.concl (Goal.assume gl) in
-    pf_apply Retyping.get_sort_family_of gl c
+    pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr c)
 
   let elimination_sort_of_hyp id gl =
     (** Retyping will expand evars anyway. *)
     let c = pf_get_hyp_typ id (Goal.assume gl) in
-    pf_apply Retyping.get_sort_family_of gl c
+    pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr c)
 
   let elimination_sort_of_clause id gl = match id with
   | None -> elimination_sort_of_goal gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c96553fae5..e294f928eb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -412,7 +412,7 @@ let default_id env sigma decl =
   let open Context.Rel.Declaration in
   match decl with
   | LocalAssum (name,t) ->
-      let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in
+      let dft = default_id_of_sort (Retyping.get_sort_of env sigma (EConstr.of_constr t)) in
       id_of_name_with_default dft name
   | LocalDef (name,b,_) -> id_of_name_using_hdchar env b name
 
@@ -784,9 +784,9 @@ let make_change_arg c pats =
   { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma }
 
 let check_types env sigma mayneedglobalcheck deep newc origc =
-  let t1 = Retyping.get_type_of env sigma newc in
+  let t1 = Retyping.get_type_of env sigma (EConstr.of_constr newc) in
   if deep then begin
-    let t2 = Retyping.get_type_of env sigma origc in
+    let t2 = Retyping.get_type_of env sigma (EConstr.of_constr origc) in
     let sigma, t2 = Evarsolve.refresh_universes
 		      ~onlyalg:true (Some false) env sigma t2 in
     let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
@@ -1341,7 +1341,7 @@ let enforce_prop_bound_names rename tac =
         | Prod (Name _ as na,t,t') ->
             let very_standard = true in
             let na =
-              if Retyping.get_sort_family_of env sigma t = InProp then
+              if Retyping.get_sort_family_of env sigma (EConstr.of_constr t) = InProp then
                 (* "very_standard" says that we should have "H" names only, but
                    this would break compatibility even more... *)
                 let s = match Namegen.head_name t with
@@ -1411,7 +1411,7 @@ let general_elim_clause_gen elimtac indclause elim =
   let env = Proofview.Goal.env gl in
   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 = Retyping.get_type_of env sigma (EConstr.of_constr elimc) in
   let i =
     match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
   elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
@@ -1421,7 +1421,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
   Proofview.Goal.enter { enter = begin fun gl ->
   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 = 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 elimtac = elimination_clause_scheme with_evars in
   let indclause  = make_clenv_binding env sigma (c, t) lbindc in
@@ -1439,7 +1439,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   let sigma = Proofview.Goal.sigma gl in
   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 = Retyping.get_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c) 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) =
@@ -1554,7 +1554,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
           (str "The type of elimination clause is not well-formed.") in
   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 = Retyping.get_type_of env sigma (EConstr.of_constr hyp) 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
@@ -1614,7 +1614,7 @@ let make_projection env sigma params cstr sign elim i n c u =
 		[|mkApp (c, args)|])
 	  in
 	  let app = it_mkLambda_or_LetIn proj sign in
-	  let t = Retyping.get_type_of env sigma app in
+	  let t = Retyping.get_type_of env sigma (EConstr.of_constr app) in
 	    Some (app, t)
       | None -> None
   in elim
@@ -1624,7 +1624,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   try
-    let t = Retyping.get_type_of env sigma c in
+    let t = Retyping.get_type_of env sigma (EConstr.of_constr c) 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
@@ -1704,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 (EConstr.of_constr (Retyping.get_type_of env sigma c)) in
+    let thm_ty0 = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) in
     let try_apply thm_ty nprod =
       try
         let n = nb_prod_modulo_zeta sigma (EConstr.of_constr thm_ty) - nprod in
@@ -1830,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 (EConstr.of_constr (Retyping.get_type_of env sigma d)) in
+  let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma (EConstr.of_constr d))) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when CErrors.noncritical e ->
@@ -2604,7 +2604,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
     let Sigma (t, sigma, p) = match ty with
     | Some t -> Sigma.here t sigma
     | None ->
-      let t = typ_of env sigma c in
+      let t = typ_of env sigma (EConstr.of_constr c) in
       let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in
       Sigma.Unsafe.of_pair (c, sigma)
     in
@@ -2656,7 +2656,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 | _ -> typ_of env sigma c in
+  let t = match ty with Some t -> t | _ -> typ_of env sigma (EConstr.of_constr c) in
   let decl = if dep then LocalDef (id,c,t)
 	     else LocalAssum (id,t)
   in
@@ -2903,7 +2903,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,Retyping.get_type_of env sigma c) lbind in
+      let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma (EConstr.of_constr 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 (EConstr.of_constr (clenv_value clause)) in
@@ -2919,7 +2919,7 @@ let specialize (c,lbind) ipat =
           pr_name (meta_name clause.evd (List.hd (collect_metas clause.evd (EConstr.of_constr term)))) ++
 	  str ".");
       clause.evd, term in
-  let typ = Retyping.get_type_of env sigma term in
+  let typ = Retyping.get_type_of env sigma (EConstr.of_constr term) in
   let tac =
     match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with
     | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) ->
@@ -3152,7 +3152,7 @@ let expand_projections env sigma c =
   let sigma = Sigma.to_evar_map sigma in
   let rec aux env c =
     match EConstr.kind sigma c with
-    | Proj (p, c) -> EConstr.of_constr (Retyping.expand_projection env sigma p (EConstr.Unsafe.to_constr (aux env c)) [])
+    | Proj (p, c) -> EConstr.of_constr (Retyping.expand_projection env sigma p (aux env c) [])
     | _ -> map_constr_with_full_binders sigma push_rel aux env c
   in
   EConstr.Unsafe.to_constr (aux env (EConstr.of_constr c))
@@ -3673,7 +3673,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 	else []
       in
       let body, c' =
-	if defined then Some c', Retyping.get_type_of ctxenv !sigma c'
+	if defined then Some c', Retyping.get_type_of ctxenv !sigma (EConstr.of_constr c')
 	else None, c'
       in
       let typ = Tacmach.pf_get_hyp_typ gl id in
@@ -4132,7 +4132,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
     let dep_in_concl = Option.cata (fun id -> occur_var env sigma id (EConstr.of_constr concl)) false hyp0 in
     let dep = dep_in_hyps || dep_in_concl in
     let tmpcl = it_mkNamedProd_or_LetIn concl deps in
-    let s = Retyping.get_sort_family_of env sigma tmpcl in
+    let s = Retyping.get_sort_family_of env sigma (EConstr.of_constr tmpcl) in
     let deps_cstr =
       List.fold_left
         (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.get_id decl))::a else a) [] deps in
@@ -4286,7 +4286,7 @@ let check_enough_applied env sigma elim =
       fun u ->
       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 elimt = Retyping.get_type_of env sigma (EConstr.of_constr (fst elimc)) in
       let scheme = compute_elim_sig ~elimc elimt in
       match scheme.indref with
       | None ->
@@ -4331,7 +4331,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
         Refine.refine ~unsafe:true { run = begin fun sigma ->
           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 = Retyping.get_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c) 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 };
@@ -4376,7 +4376,7 @@ let induction_gen clear_flag isrec with_evars elim
   let sigma = Proofview.Goal.sigma gl in
   let ccl = Proofview.Goal.raw_concl gl in
   let cls = Option.default allHypsAndConcl cls in
-  let t = typ_of env sigma c in
+  let t = typ_of env sigma (EConstr.of_constr c) in
   let is_arg_pure_hyp =
     isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ()))
     && lbind == NoBindings && not with_evars && Option.is_empty eqname