Removing various compatibility layers of tactics.

2 files changed, 16 insertions, 13 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8d4d87f2a2..e5dd6a6ec3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1982,7 +1982,7 @@ let interp_type env sigma ?(impls=empty_internalization_env) c =
   interp_gen IsType env sigma ~impls c
 
 let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ =
-  interp_gen (OfType (EConstr.of_constr typ)) env sigma ~impls c
+  interp_gen (OfType typ) env sigma ~impls c
 
 (* Not all evars expected to be resolved *)
 
@@ -2001,7 +2001,7 @@ let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c
 
 let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen_impls env evdref ~impls (OfType (EConstr.of_constr typ)) c
+  interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c
 
 let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen_impls env evdref ~impls IsType c
@@ -2093,6 +2093,7 @@ let interp_rawcontext_evars env evdref k bl =
        let t = understand_tcc_evars env evdref ~expected_type:IsType t' in
 	match b with
 	    None ->
+              let t = EConstr.Unsafe.to_constr t in
 	      let d = LocalAssum (na,t) in
 	      let impls =
 		if k == Implicit then
@@ -2102,7 +2103,9 @@ let interp_rawcontext_evars env evdref k bl =
 	      in
 		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
-	      let c = understand_tcc_evars env evdref ~expected_type:(OfType (EConstr.of_constr t)) b in
+	      let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in
+              let t = EConstr.Unsafe.to_constr t in
+              let c = EConstr.Unsafe.to_constr c in
 	      let d = LocalDef (na, c, t) in
 		(push_rel d env, d::params, n, impls))
       (env,[],k+1,[]) (List.rev bl)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 61e7c6f5cb..2f6795ed48 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -101,7 +101,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> constr Evd.in_evar_universe_context
 
 val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
-  constr_expr -> types -> constr Evd.in_evar_universe_context
+  constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context
 
 val interp_type : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> types Evd.in_evar_universe_context
@@ -109,32 +109,32 @@ val interp_type : env -> evar_map -> ?impls:internalization_env ->
 (** Main interpretation function expecting all postponed problems to
     be resolved, but possibly leaving evars. *)
 
-val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
+val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr
 
 (** Accepting unresolved evars *)
 
 val interp_constr_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> constr
+  ?impls:internalization_env -> constr_expr -> EConstr.constr
 
 val interp_casted_constr_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> types -> constr
+  ?impls:internalization_env -> constr_expr -> types -> EConstr.constr
 
 val interp_type_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> types
+  ?impls:internalization_env -> constr_expr -> EConstr.types
 
 (** Accepting unresolved evars and giving back the manual implicit arguments *)
 
 val interp_constr_evars_impls : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr ->
-  constr * Impargs.manual_implicits
+  EConstr.constr * Impargs.manual_implicits
 
 val interp_casted_constr_evars_impls : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> types ->
-  constr * Impargs.manual_implicits
+  ?impls:internalization_env -> constr_expr -> EConstr.types ->
+  EConstr.constr * Impargs.manual_implicits
 
 val interp_type_evars_impls : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr ->
-  types * Impargs.manual_implicits
+  EConstr.types * Impargs.manual_implicits
 
 (** Interprets constr patterns *)
 
@@ -153,7 +153,7 @@ val interp_reference : ltac_sign -> reference -> glob_constr
 val interp_binder  : env -> evar_map -> Name.t -> constr_expr -> 
   types Evd.in_evar_universe_context
 
-val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
+val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types
 
 (** Interpret contexts: returns extended env and context *)