Typing API using EConstr.

10 files changed, 37 insertions, 37 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 36a96fdb5..58454eedf 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -50,7 +50,7 @@ let whd_delta env=
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = e_sort_of env (ref sigma) c
+let sf_of env sigma c = e_sort_of env (ref sigma) (EConstr.of_constr c)
 
 let rec decompose_term env sigma t=
     match kind_of_term (whd env t) with
@@ -247,7 +247,7 @@ let new_refine c = Proofview.V82.tactic (refine c)
 
 let assert_before n c =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let evm, _ = Tacmach.New.pf_apply type_of gl c in
+    let evm, _ = Tacmach.New.pf_apply type_of gl (EConstr.of_constr c) in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
   end }
 
@@ -340,7 +340,7 @@ let refute_tac c t1 t2 p =
   end }
 
 let refine_exact_check c gl =
-  let evm, _ = pf_apply type_of gl c in
+  let evm, _ = pf_apply type_of gl (EConstr.of_constr c) in
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
@@ -480,10 +480,10 @@ let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
-    let evm, ty = pf_apply type_of gl c1 in
+    let evm, ty = pf_apply type_of gl (EConstr.of_constr c1) in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm (EConstr.of_constr ty) in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
-    let evm, _ =  type_of (pf_env gl) evm term in
+    let evm, _ =  type_of (pf_env gl) evm (EConstr.of_constr term) in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
 			  (k term)
     end })
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c17c8dbb8..dcebf7806 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -429,7 +429,7 @@ let concl_refiner metas body gls =
   let concl = pf_concl gls in
   let evd = sig_sig gls in
   let env = pf_env gls in
-  let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
+  let sort = family_of_sort (Typing.e_sort_of env (ref evd) (EConstr.of_constr concl)) in
   let rec aux env avoid subst = function
       [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
     | (n,typ)::rest ->
@@ -437,7 +437,7 @@ let concl_refiner metas body gls =
 	let x = id_of_name_using_hdchar env _A Anonymous in
 	let _x = fresh_id avoid x gls in
 	let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
-	let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in
+	let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) (EConstr.of_constr _A)) in
 	let nsubst = (n,mkVar _x)::subst in
 	  if List.is_empty rest then
 	    asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a3513692c..44bdb585a 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -155,7 +155,7 @@ let left_instance_tac (inst,id) continue seq=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
 		  let evmap, _ =
-		    try Typing.type_of (pf_env gl) evmap gt
+		    try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt)
 		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 340dd2c28..0a7938069 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -329,7 +329,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	   let all_ids = pf_ids_of_hyps g in
 	   let new_ids,_  = list_chop ctxt_size all_ids in
 	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
-	   let evm, _ = pf_apply Typing.type_of g to_refine in
+	   let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr to_refine) in
 	     tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
 	)
     in
@@ -544,7 +544,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
       tclIDTAC
   in
   try
-    scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
+    scan_type [] (Typing.unsafe_type_of env sigma (EConstr.mkVar hyp_id)), [hyp_id]
   with TOREMOVE ->
     thin [hyp_id],[]
 
@@ -639,7 +639,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  let c = mkApp(mkVar hid,args) in
-	  let evm, _ = pf_apply Typing.type_of g c in
+	  let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr c) in
 	  tclTHENLIST[
             Refiner.tclEVARS evm;
 	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
@@ -968,7 +968,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
   (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
   let (type_ctxt,type_of_f),evd =
-    let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
+    let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f)
     in 
     decompose_prod_n_assum
       (nb_params + nb_args) t,evd
@@ -1039,7 +1039,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
       in
       evd:=evd';                       
-      let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
+      let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr res) in 
       res
   in
   let nb_intro_to_do = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9637632a6..4b47b83af 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -283,7 +283,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   let new_princ_name =
     next_ident_away_in_goal (Id.of_string "___________princ_________") []
   in
-  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in
+  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
     Lemmas.start_proof
@@ -337,7 +337,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 	let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
-	let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in
+	let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
 	(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
 	let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
 	ignore(
@@ -488,7 +488,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
   in
   let _ = evd := sigma in 
   let l_schemes =
-    List.map (Typing.unsafe_type_of env sigma) schemes
+    List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma) schemes
   in
   let i = ref (-1) in
   let sorts =
@@ -616,7 +616,7 @@ let build_scheme fas =
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
             let _ = evd := evd' in 
-	    let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in 
+	    let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in 
 	    (destConst f,sort)
 	 )
 	 fas
@@ -666,7 +666,7 @@ let build_case_scheme fa =
       Indrec.build_case_analysis_scheme_default env sigma ind sf
   in
   let sigma = Sigma.to_evar_map sigma in
-  let scheme_type =  (Typing.unsafe_type_of env sigma ) scheme in
+  let scheme_type =  (Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme) in
   let sorts =
     (fun (_,_,x) ->
        Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 92de4d873..38cd21684 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -503,7 +503,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		   The "value" of this branch is then simply [res]
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
-		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
+		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
 		let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
@@ -611,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	*)
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
-	let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
+	let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
 	let new_env =
 	  match n with
 	      Anonymous -> env
@@ -627,7 +627,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	build_entry_lc_from_case env funnames make_discr el brl avoid
     | GIf(_,b,(na,e_option),lhs,rhs) ->
 	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
 	let (ind,_) =
 	  try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
 	  with Not_found ->
@@ -659,7 +659,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	      nal
 	  in
 	  let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-	  let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+	  let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
 	  let (ind,_) =
 	    try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
 	    with Not_found ->
@@ -706,7 +706,7 @@ and build_entry_lc_from_case env funname make_discr
 	let types =
 	  List.map (fun (case_arg,_) ->
 		      let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
-		      Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr
+		      Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr)
 		   ) el
 	in
 	(****** The next works only if the match is not dependent ****)
@@ -753,7 +753,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		   List.fold_right
 		     (fun id acc ->
 			let typ_of_id =
-			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id)
+			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
 			in
 			let raw_typ_of_id =
 			  Detyping.detype false []
@@ -807,7 +807,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		   (fun id  acc ->
 		      if Id.Set.mem id this_pat_ids
 		      then (Prod (Name id),
-		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (mkVar id) in
+		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
 		      let raw_typ_of_id =
 			Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
 		      in
@@ -1121,7 +1121,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let evd = (Evd.from_env env) in
 	  let t',ctx = Pretyping.understand env evd t in
 	  let evd = Evd.from_ctx ctx in
-	  let type_t' = Typing.unsafe_type_of env evd t' in
+	  let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr t') in
 	  let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
@@ -1272,7 +1272,7 @@ let do_build_inductive
   let evd,env =
     Array.fold_right2
       (fun id c (evd,env) ->
-       let evd,t = Typing.type_of env evd (mkConstU c) in
+       let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in
        evd,
        Environ.push_named (LocalAssum (id,t))
 			   (* try *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a264c37c5..0743fc5d9 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -369,7 +369,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	     let evd = ref (Evd.from_env env) in
 	     let evd',uprinc = Evd.fresh_global env !evd princ in
              let _ = evd := evd' in 
-	     let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in
+	     let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in
     	     Functional_principles_types.generate_functional_principle
 	       evd
 		 interactive_proof
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 9abe60402..e5286fb1f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -134,7 +134,7 @@ let generate_type evd g_to_f f graph i =
     Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd graph)))
   in
   evd:=evd';
-  let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+  let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -202,7 +202,7 @@ let find_induction_principle evd f =
     | None -> raise Not_found
     | Some rect_lemma ->
        let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
-       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in
        evd:=evd';
        rect_lemma,typ
 
@@ -449,7 +449,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	     "functional_induction" (
 	       (fun gl ->
 		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
+		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl (EConstr.of_constr term) in
 		Proofview.V82.of_tactic (apply term) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
@@ -792,7 +792,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
+	 let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in 
 	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4fd9e0ff8..12ed758ba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -657,7 +657,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
   continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} 
 
 let pf_type c tac gl = 
-  let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
+  let evars, ty = Typing.type_of (pf_env gl) (project gl) (EConstr.of_constr c) in
     tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
 
 let pf_typel l tac =
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e1b95ddbc..b0a3e839b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -493,8 +493,8 @@ let ring_equality env evd (r,add,mul,opp,req) =
 	  match opp with
               Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
             | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
-	let setoid = Typing.e_solve_evars env evd setoid in
-	let op_morph = Typing.e_solve_evars env evd op_morph in
+	let setoid = Typing.e_solve_evars env evd (EConstr.of_constr setoid) in
+	let op_morph = Typing.e_solve_evars env evd (EConstr.of_constr op_morph) in
 	  (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) evd r req in
@@ -581,7 +581,7 @@ let make_hyp_list env evd lH =
       (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
       (plapp evd coq_nil [|carrier|])
   in 
-  let l' = Typing.e_solve_evars env evd l in
+  let l' = Typing.e_solve_evars env evd (EConstr.of_constr l) in
     Evarutil.nf_evars_universes !evd l'
 
 let interp_power env evd pow =
@@ -707,7 +707,7 @@ let make_term_list env evd carrier rl =
   let l = List.fold_right
     (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
     (plapp evd coq_nil [|carrier|])
-  in Typing.e_solve_evars env evd l
+  in Typing.e_solve_evars env evd (EConstr.of_constr l)
 
 let carg = Tacinterp.Value.of_constr
 let tacarg expr =