Removing various compatibility layers of tactics.

10 files changed, 36 insertions, 33 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 565a9725c2..eea94f021e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2076,7 +2076,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	let IndType (indf, _) = 
 	  try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty)
 	  with Not_found -> error_case_not_inductive env !evdref
-	    {uj_val = ty; uj_type = EConstr.of_constr (Typing.unsafe_type_of env !evdref ty)}
+	    {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty}
 	in
 	let (ind,u), params = dest_ind_family indf in
 	let params = List.map EConstr.of_constr params in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index a42061f283..e18625c427 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -377,7 +377,7 @@ and cbv_norm_value info = function (* reduction under binders *)
 (* with profiling *)
 let cbv_norm infos constr =
   let constr = EConstr.Unsafe.to_constr constr in
-  with_stats (lazy (cbv_norm_term infos (subs_id 0) constr))
+  EConstr.of_constr (with_stats (lazy (cbv_norm_term infos (subs_id 0) constr)))
 
 type cbv_infos = cbv_value infos
 
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 3d17457679..b014af2c7f 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open EConstr
 open Environ
 open CClosure
 open Esubst
@@ -19,10 +20,13 @@ open Esubst
 type cbv_infos
 
 val create_cbv_infos : RedFlags.reds -> env -> Evd.evar_map -> cbv_infos
-val cbv_norm         : cbv_infos -> EConstr.constr -> constr
+val cbv_norm         : cbv_infos -> constr -> constr
 
 (***********************************************************************
   i This is for cbv debug *)
+
+open Term
+
 type cbv_value =
   | VAL of int * constr
   | STACK of int * cbv_value * cbv_stack
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f569d9fc4a..ead44cee2f 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -194,7 +194,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	else Some (fun x -> 
 	  let term = co x in
-	    EConstr.of_constr (Typing.e_solve_evars env evdref term))
+	    Typing.e_solve_evars env evdref term)
       in
 	if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then
 	  (* Second-order unification needed. *)
@@ -302,7 +302,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 		      with NoSubtacCoercion ->
 			let typ = Typing.unsafe_type_of env evm c in
 			let typ' = Typing.unsafe_type_of env evm c' in
-			  coerce_application (EConstr.of_constr typ) (EConstr.of_constr typ') c c' l l')
+			  coerce_application typ typ' c c' l l')
 		 else
 		   subco ()
 	   | x, y when EConstr.eq_constr !evdref c c' ->
@@ -310,7 +310,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 		 let evm =  !evdref in
 		 let lam_type = Typing.unsafe_type_of env evm c in
 		 let lam_type' = Typing.unsafe_type_of env evm c' in
-		   coerce_application (EConstr.of_constr lam_type) (EConstr.of_constr lam_type') c c' l l'
+		   coerce_application lam_type lam_type' c c' l l'
 	       else subco ()
 	   | _ -> subco ())
       | _, _ ->  subco ()
@@ -341,7 +341,7 @@ let app_coercion env evdref coercion v =
   | None -> v
   | Some f ->
      let v' = Typing.e_solve_evars env evdref (f v) in
-     whd_betaiota !evdref (EConstr.of_constr v')
+     whd_betaiota !evdref v'
 
 let coerce_itf loc env evd v t c1 =
   let evdref = ref evd in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 09b99983cc..f76f608d0d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -524,7 +524,6 @@ let pretype_ref loc evdref env ref us =
     let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
     let ty = unsafe_type_of env.ExtraEnv.env evd c in
-    let ty = EConstr.of_constr ty in
       make_judge c ty
 
 let judge_of_Type loc evd s =
@@ -1194,16 +1193,16 @@ let understand
 
 let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c =
   let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in
-  (sigma, EConstr.Unsafe.to_constr c)
+  (sigma, c)
 
 let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c =
   let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in
   evdref := sigma;
-  EConstr.Unsafe.to_constr c
+  c
 
 let understand_ltac flags env sigma lvar kind c =
   let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in
-  (sigma, EConstr.Unsafe.to_constr c)
+  (sigma, c)
 
 let constr_flags = {
   use_typeclasses = true;
@@ -1225,7 +1224,6 @@ let type_uconstr ?(flags = constr_flags)
   } in
   let sigma = Sigma.to_evar_map sigma in
   let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
-  let c = EConstr.of_constr c in
   Sigma.Unsafe.of_pair (c, sigma)
   end }
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index a1602088ab..825d73f1f1 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -76,10 +76,10 @@ val allow_anonymous_refs : bool ref
     evar_map is modified explicitly or by side-effect. *)
 
 val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
-  ?expected_type:typing_constraint -> glob_constr -> open_constr
+  ?expected_type:typing_constraint -> glob_constr -> evar_map * EConstr.constr
 
 val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
-  ?expected_type:typing_constraint -> glob_constr -> constr
+  ?expected_type:typing_constraint -> glob_constr -> EConstr.constr
 
 (** More general entry point with evars from ltac *)
 
@@ -95,7 +95,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
 
 val understand_ltac : inference_flags ->
   env -> evar_map -> ltac_var_map ->
-  typing_constraint -> glob_constr -> pure_open_constr
+  typing_constraint -> glob_constr -> evar_map * EConstr.constr
 
 (** Standard call to get a constr from a glob_constr, resolving
     implicit arguments and coercions, and compiling pattern-matching;
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 3fc01c86c6..2b496f9267 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1133,7 +1133,7 @@ let fold_commands cl env sigma c =
 
 (* call by value reduction functions *)
 let cbv_norm_flags flags env sigma t =
-  EConstr.of_constr (cbv_norm (create_cbv_infos flags env sigma) t)
+  cbv_norm (create_cbv_infos flags env sigma) t
 
 let cbv_beta = cbv_norm_flags beta empty_env
 let cbv_betaiota = cbv_norm_flags betaiota empty_env
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index d24160ea54..7baff421fb 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -376,7 +376,7 @@ let unsafe_type_of env evd c =
   let evdref = ref evd in
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-    EConstr.Unsafe.to_constr j.uj_type
+    j.uj_type
 
 (* Sort of a type *)
 
@@ -411,6 +411,6 @@ let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
-  nf_evar !evdref (EConstr.Unsafe.to_constr c)
+  EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr c))
 
-let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c))
+let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index bf26358a22..91134b4999 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -9,46 +9,47 @@
 open Names
 open Term
 open Environ
+open EConstr
 open Evd
 
 (** This module provides the typing machine with existential variables
     and universes. *)
 
 (** Typecheck a term and return its type. May trigger an evarmap leak. *)
-val unsafe_type_of : env -> evar_map -> EConstr.constr -> types
+val unsafe_type_of : env -> evar_map -> constr -> types
 
 (** Typecheck a term and return its type + updated evars, optionally refreshing
     universes *)
-val type_of : ?refresh:bool -> env -> evar_map -> EConstr.constr -> evar_map * EConstr.types
+val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 
 (** Variant of [type_of] using references instead of state-passing. *)
-val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> EConstr.types
+val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
 
 (** Typecheck a type and return its sort *)
-val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts
+val e_sort_of : env -> evar_map ref -> types -> sorts
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
-val e_check   : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit
+val e_check   : env -> evar_map ref -> constr -> types -> unit
 
 (** Returns the instantiated type of a metavariable *)
-val meta_type : evar_map -> metavariable -> EConstr.types
+val meta_type : evar_map -> metavariable -> types
 
 (** Solve existential variables using typing *)
-val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr
+val e_solve_evars : env -> evar_map ref -> constr -> constr
 
 (** Raise an error message if incorrect elimination for this inductive *)
 (** (first constr is term to match, second is return predicate) *)
-val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> EConstr.constr ->
+val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
   unit
 
 (** Raise an error message if bodies have types not unifiable with the
     expected ones *)
 val check_type_fixpoint : Loc.t -> env -> evar_map ref ->
-  Names.Name.t array -> EConstr.types array -> EConstr.unsafe_judgment array -> unit
+  Names.Name.t array -> types array -> unsafe_judgment array -> unit
 
-val judge_of_prop : EConstr.unsafe_judgment
-val judge_of_set : EConstr.unsafe_judgment
+val judge_of_prop : unsafe_judgment
+val judge_of_set : unsafe_judgment
 val judge_of_abstraction : Environ.env -> Name.t ->
-  EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
+  unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment
 val judge_of_product : Environ.env -> Name.t ->
-  EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment
+  unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c6fad1a349..5bb865310c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1228,7 +1228,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
       | _ -> error "Apply_Head_Then"
   in
-    apprec n c (EConstr.of_constr (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c)) Sigma.refl evd
+    apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd
 
 let is_mimick_head sigma ts f =
   match EConstr.kind sigma f with