Cleaning up interfaces.

We make mli files look to what they were looking before the move to EConstr
by opening this module.

11 files changed, 99 insertions, 96 deletions

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 15409f2b86..d09686f6e2 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -141,8 +141,8 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
 let replace_term_occ_modulo evd occs test bywhat t =
   let occs',like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
-  EConstr.Unsafe.to_constr (proceed_with_occurrences
-    (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t)
+  proceed_with_occurrences
+    (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t
 
 let replace_term_occ_decl_modulo evd occs test bywhat d =
   let (plocs,hyploc),like_first =
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index c7db84e3c7..3d2ebb72df 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -11,11 +11,12 @@ open Term
 open Evd
 open Pretype_errors
 open Environ
+open EConstr
 
 (** Finding subterms, possibly up to some unification function,
     possibly at some given occurrences *)
 
-exception NotUnifiable of (EConstr.constr * EConstr.constr * unification_error) option
+exception NotUnifiable of (constr * constr * unification_error) option
 
 exception SubtermUnificationError of subterm_unification_error
 
@@ -26,7 +27,7 @@ exception SubtermUnificationError of subterm_unification_error
     with None. *)
 
 type 'a testing_function = {
-  match_fun : 'a -> EConstr.constr -> 'a;
+  match_fun : 'a -> constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
   mutable testing_state : 'a;
   mutable last_found : position_reporting option
@@ -34,7 +35,7 @@ type 'a testing_function = {
 
 (** This is the basic testing function, looking for exact matches of a
     closed term *)
-val make_eq_univs_test : env -> evar_map -> EConstr.constr -> evar_map testing_function
+val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
 
 (** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm
     modulo a testing function [test] and replaces successfully
@@ -42,27 +43,27 @@ val make_eq_univs_test : env -> evar_map -> EConstr.constr -> evar_map testing_f
     ()]; it turns a NotUnifiable exception raised by the testing
     function into a SubtermUnificationError. *)
 val replace_term_occ_modulo : evar_map -> occurrences or_like_first ->
-  'a testing_function -> (unit -> EConstr.constr) -> EConstr.constr -> constr
+  'a testing_function -> (unit -> constr) -> constr -> constr
 
 (** [replace_term_occ_decl_modulo] is similar to
     [replace_term_occ_modulo] but for a named_declaration. *)
 val replace_term_occ_decl_modulo :
   evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
-  'a testing_function -> (unit -> EConstr.constr) ->
+  'a testing_function -> (unit -> constr) ->
   Context.Named.Declaration.t -> Context.Named.Declaration.t
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of
     closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
     unifying universes which results in a set of constraints. *)
 val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
-  EConstr.constr -> EConstr.constr -> constr * evar_map
+  constr -> constr -> constr * evar_map
 
 (** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of 
     closed [c] at positions [occl] by [Rel 1] in [decl]. *)
 val subst_closed_term_occ_decl : env -> evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
-  EConstr.constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map
+  constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map
 
 (** Miscellaneous *)
 val error_invalid_occurrence : int list -> 'a
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 0ebe4817ca..7cef14339b 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -9,52 +9,53 @@
 open Names
 open Term
 open Environ
+open EConstr
 open Type_errors
 
 (** {6 The type of errors raised by the pretyper } *)
 
 type unification_error =
-  | OccurCheck of existential_key * EConstr.constr
-  | NotClean of EConstr.existential * env * EConstr.constr
+  | OccurCheck of existential_key * constr
+  | NotClean of existential * env * constr
   | NotSameArgSize
   | NotSameHead
   | NoCanonicalStructure
-  | ConversionFailed of env * EConstr.constr * EConstr.constr
+  | ConversionFailed of env * constr * constr
   | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types
+  | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
   | CannotSolveConstraint of Evd.evar_constraint * unification_error
   | ProblemBeyondCapabilities
 
 type position = (Id.t * Locus.hyp_location_flag) option
 
-type position_reporting = (position * int) * EConstr.t
+type position_reporting = (position * int) * constr
 
-type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option
+type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option
 
-type type_error = (EConstr.constr, EConstr.types) ptype_error
+type type_error = (constr, types) ptype_error
 
 type pretype_error =
   (** Old Case *)
-  | CantFindCaseType of EConstr.constr
+  | CantFindCaseType of constr
   (** Type inference unification *)
-  | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
+  | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
   (** Tactic Unification *)
-  | UnifOccurCheck of existential_key * EConstr.constr
+  | UnifOccurCheck of existential_key * constr
   | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
-  | CannotUnify of EConstr.constr * EConstr.constr * unification_error option
-  | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr
-  | CannotUnifyBindingType of constr * constr
-  | CannotGeneralize of constr
-  | NoOccurrenceFound of EConstr.constr * Id.t option
-  | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (env * type_error) option
-  | WrongAbstractionType of Name.t * EConstr.constr * EConstr.types * EConstr.types
+  | CannotUnify of constr * constr * unification_error option
+  | CannotUnifyLocal of constr * constr * constr
+  | CannotUnifyBindingType of Constr.constr * Constr.constr
+  | CannotGeneralize of Constr.constr
+  | NoOccurrenceFound of constr * Id.t option
+  | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+  | WrongAbstractionType of Name.t * constr * types * types
   | AbstractionOverMeta of Name.t * Name.t
-  | NonLinearUnification of Name.t * EConstr.constr
+  | NonLinearUnification of Name.t * constr
   (** Pretyping *)
   | VarNotFound of Id.t
-  | UnexpectedType of EConstr.constr * EConstr.constr
-  | NotProduct of EConstr.constr
+  | UnexpectedType of constr * constr
+  | NotProduct of constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
   | UnsatisfiableConstraints of
@@ -67,85 +68,85 @@ val precatchable_exception : exn -> bool
 
 (** Raising errors *)
 val error_actual_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr ->
+  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
       unification_error -> 'b
 
 val error_actual_type_core :
-  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
+      unsafe_judgment -> unsafe_judgment array -> 'b
 
 val error_cant_apply_bad_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> int * EConstr.constr * EConstr.constr ->
-      EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr ->
+      unsafe_judgment -> unsafe_judgment array -> 'b
 
 val error_case_not_inductive :
-  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_ill_formed_branch :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      EConstr.constr -> pconstructor -> EConstr.constr -> EConstr.constr -> 'b
+      constr -> pconstructor -> constr -> constr -> 'b
 
 val error_number_branches :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      EConstr.unsafe_judgment -> int -> 'b
+      unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      int -> Name.t array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b
+      int -> Name.t array -> unsafe_judgment array -> types array -> 'b
 
 val error_elim_arity :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      pinductive -> sorts_family list -> EConstr.constr ->
-      EConstr.unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b
+      pinductive -> sorts_family list -> constr ->
+      unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b
 
 val error_not_a_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_assumption :
-  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
-val error_cannot_coerce : env -> Evd.evar_map -> EConstr.constr * EConstr.constr -> 'b
+val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
 (** {6 Implicit arguments synthesis errors } *)
 
-val error_occur_check : env -> Evd.evar_map -> existential_key -> EConstr.constr -> 'b
+val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_unsolvable_implicit :
   ?loc:Loc.t -> env -> Evd.evar_map -> existential_key ->
       Evd.unsolvability_explanation option -> 'b
 
 val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map ->
-  ?reason:unification_error -> EConstr.constr * EConstr.constr -> 'b
+  ?reason:unification_error -> constr * constr -> 'b
 
-val error_cannot_unify_local : env -> Evd.evar_map -> EConstr.constr * EConstr.constr * EConstr.constr -> 'b
+val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
 
 val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
-      EConstr.constr -> EConstr.constr list -> (env * type_error) option -> 'b
+      constr -> constr list -> (env * type_error) option -> 'b
 
 val error_wrong_abstraction_type :  env -> Evd.evar_map ->
-      Name.t -> EConstr.constr -> EConstr.types -> EConstr.types -> 'b
+      Name.t -> constr -> types -> types -> 'b
 
 val error_abstraction_over_meta : env -> Evd.evar_map ->
   metavariable -> metavariable -> 'b
 
 val error_non_linear_unification : env -> Evd.evar_map ->
-  metavariable -> EConstr.constr -> 'b
+  metavariable -> constr -> 'b
 
 (** {6 Ml Case errors } *)
 
 val error_cant_find_case_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Pretyping errors } *)
 
 val error_unexpected_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b
 
 val error_not_product :
-  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Error in conversion from AST to glob_constr } *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f76f608d0d..6b6800ac6a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -61,7 +61,7 @@ type ltac_var_map = {
   ltac_genargs : unbound_ltac_var_map;
 }
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
-type pure_open_constr = evar_map * Constr.constr
+type pure_open_constr = evar_map * EConstr.constr
 
 (************************************************************************)
 (* This concerns Cases *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 825d73f1f1..47ad93d7e0 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -16,6 +16,7 @@ open Names
 open Term
 open Environ
 open Evd
+open EConstr
 open Glob_term
 open Evarutil
 open Misctypes
@@ -25,7 +26,7 @@ open Misctypes
 val search_guard :
   Loc.t -> env -> int list list -> rec_declaration -> int array
 
-type typing_constraint = OfType of EConstr.types | IsType | WithoutTypeConstraint
+type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
 type var_map = Pattern.constr_under_binders Id.Map.t
 type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
@@ -47,7 +48,7 @@ val empty_lvar : ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
-type inference_hook = env -> evar_map -> evar -> evar_map * EConstr.constr
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
   use_typeclasses : bool;
@@ -76,10 +77,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 -> evar_map * EConstr.constr
+  ?expected_type:typing_constraint -> glob_constr -> evar_map * constr
 
 val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
-  ?expected_type:typing_constraint -> glob_constr -> EConstr.constr
+  ?expected_type:typing_constraint -> glob_constr -> constr
 
 (** More general entry point with evars from ltac *)
 
@@ -95,7 +96,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 -> evar_map * EConstr.constr
+  typing_constraint -> glob_constr -> pure_open_constr
 
 (** Standard call to get a constr from a glob_constr, resolving
     implicit arguments and coercions, and compiling pattern-matching;
@@ -105,21 +106,21 @@ val understand_ltac : inference_flags ->
     unresolved evar remains, expanding evars. *)
 
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
-  env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
+  env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context
 
 (** Idem but returns the judgment of the understood term *)
 
 val understand_judgment : env -> evar_map -> 
-  glob_constr -> EConstr.unsafe_judgment Evd.in_evar_universe_context
+  glob_constr -> unsafe_judgment Evd.in_evar_universe_context
 
 (** Idem but do not fail on unresolved evars (type cl*)
 val understand_judgment_tcc : env -> evar_map ref ->
-  glob_constr -> EConstr.unsafe_judgment
+  glob_constr -> unsafe_judgment
 
 val type_uconstr :
   ?flags:inference_flags ->
   ?expected_type:typing_constraint ->
-  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open
+  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
 
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
@@ -139,21 +140,21 @@ val check_evars_are_solved :
 
 (** [check_evars env initial_sigma extended_sigma c] fails if some
    new unresolved evar remains in [c] *)
-val check_evars : env -> evar_map -> evar_map -> EConstr.constr -> unit
+val check_evars : env -> evar_map -> evar_map -> constr -> unit
 
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
   int -> bool -> type_constraint -> env -> evar_map ref ->
-  ltac_var_map -> glob_constr -> EConstr.unsafe_judgment
+  ltac_var_map -> glob_constr -> unsafe_judgment
 
 val pretype_type :
   int -> bool -> val_constraint -> env -> evar_map ref ->
-  ltac_var_map -> glob_constr -> EConstr.unsafe_type_judgment
+  ltac_var_map -> glob_constr -> unsafe_type_judgment
 
 val ise_pretype_gen :
   inference_flags -> env -> evar_map ->
-  ltac_var_map -> typing_constraint -> glob_constr -> evar_map * EConstr.constr
+  ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr
 
 (**/**)
 
@@ -163,5 +164,5 @@ val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
 val interp_elimination_sort : glob_sort -> sorts_family
 
 val genarg_interp_hook :
-  (EConstr.types -> env -> evar_map -> unbound_ltac_var_map ->
-    Genarg.glob_generic_argument -> EConstr.constr * evar_map) Hook.t
+  (types -> env -> evar_map -> unbound_ltac_var_map ->
+    Genarg.glob_generic_argument -> constr * evar_map) Hook.t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2b496f9267..4abfc26fc5 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1154,7 +1154,6 @@ let abstract_scheme env sigma (locc,a) (c, sigma) =
     mkLambda (na,ta,c), sigma
   else
     let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in
-    let c' = EConstr.of_constr c' in
       mkLambda (na,ta,c'), sigma'
 
 let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 15b4e990d8..a4499015d2 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -10,6 +10,7 @@ open Names
 open Term
 open Environ
 open Evd
+open EConstr
 open Reductionops
 open Pattern
 open Globnames
@@ -17,7 +18,7 @@ open Locus
 open Univ
 
 type reduction_tactic_error =
-    InvalidAbstraction of env * evar_map * EConstr.constr * (env * Type_errors.type_error)
+    InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error)
 
 exception ReductionTacticError of reduction_tactic_error
 
@@ -58,10 +59,10 @@ val unfoldn :
   (occurrences * evaluable_global_reference) list ->  reduction_function
 
 (** Fold *)
-val fold_commands : EConstr.constr list ->  reduction_function
+val fold_commands : constr list ->  reduction_function
 
 (** Pattern *)
-val pattern_occs : (occurrences * EConstr.constr) list -> e_reduction_function
+val pattern_occs : (occurrences * constr) list -> e_reduction_function
 
 (** Rem: Lazy strategies are defined in Reduction *)
 
@@ -75,23 +76,23 @@ val cbv_norm_flags : CClosure.RedFlags.reds ->  reduction_function
 (** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
    with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_atomic_ind : env ->  evar_map -> EConstr.types -> pinductive * EConstr.types
+val reduce_to_atomic_ind : env ->  evar_map -> types -> pinductive * types
 
 (** [reduce_to_quantified_ind env sigma t] puts [t] in the form
    [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_quantified_ind : env ->  evar_map -> EConstr.types -> pinductive * EConstr.types
+val reduce_to_quantified_ind : env ->  evar_map -> types -> pinductive * types
 
 (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
    [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
 val reduce_to_quantified_ref :
-  env ->  evar_map -> global_reference -> EConstr.types -> EConstr.types
+  env ->  evar_map -> global_reference -> types -> types
 
 val reduce_to_atomic_ref :
-  env ->  evar_map -> global_reference -> EConstr.types -> EConstr.types
+  env ->  evar_map -> global_reference -> types -> types
 
 val find_hnf_rectype : 
-  env ->  evar_map -> EConstr.types -> pinductive * EConstr.constr list
+  env ->  evar_map -> types -> pinductive * constr list
 
 val contextually : bool -> occurrences * constr_pattern ->
   (patvar_map -> reduction_function) -> reduction_function
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5bb865310c..20f27a15a2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -100,7 +100,6 @@ let abstract_scheme env evd c l lname_typ =
        if occur_meta evd a then mkLambda_name env (na,ta,t), evd
        else
 	 let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in
-	 let t' = EConstr.of_constr t' in
 	   mkLambda_name env (na,ta,t'), evd')
     (c,evd)
     (List.rev l)
@@ -1656,7 +1655,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       | NoOccurrences -> concl
       | occ ->
           let occ = if likefirst then LikeFirst else AtOccs occ in
-          EConstr.of_constr (replace_term_occ_modulo sigma occ test mkvarid concl)
+          replace_term_occ_modulo sigma occ test mkvarid concl
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 58b82002da..26d4ac994b 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -8,11 +8,12 @@
 
 open Names
 open Term
+open EConstr
 open Constrexpr
 open Misctypes
 
 val lemInv_clause :
-  quantified_hypothesis -> EConstr.constr -> Id.t list -> unit Proofview.tactic
+  quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
 
 val add_inversion_lemma_exn :
   Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> unit Proofview.tactic) ->
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index e4f110722b..ba5452e33f 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -9,6 +9,7 @@
 open Pp
 open Names
 open Term
+open EConstr
 open Tacmach
 open Proof_type
 open Locus
@@ -58,25 +59,25 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 (** {6 Tacticals applying to hypotheses } *)
 
 val onNthHypId       : int -> (Id.t -> tactic) -> tactic
-val onNthHyp         : int -> (EConstr.constr -> tactic) -> tactic
+val onNthHyp         : int -> (constr -> tactic) -> tactic
 val onNthDecl        : int -> (Context.Named.Declaration.t -> tactic) -> tactic
 val onLastHypId      : (Id.t -> tactic) -> tactic
-val onLastHyp        : (EConstr.constr -> tactic) -> tactic
+val onLastHyp        : (constr -> tactic) -> tactic
 val onLastDecl       : (Context.Named.Declaration.t -> tactic) -> tactic
 val onNLastHypsId    : int -> (Id.t list -> tactic) -> tactic
-val onNLastHyps      : int -> (constr list -> tactic) -> tactic
+val onNLastHyps      : int -> (Constr.constr list -> tactic) -> tactic
 val onNLastDecls     : int -> (Context.Named.t -> tactic) -> tactic
 
 val lastHypId   : goal sigma -> Id.t
-val lastHyp     : goal sigma -> EConstr.constr
+val lastHyp     : goal sigma -> constr
 val lastDecl    : goal sigma -> Context.Named.Declaration.t
 val nLastHypsId : int -> goal sigma -> Id.t list
-val nLastHyps   : int -> goal sigma -> constr list
+val nLastHyps   : int -> goal sigma -> Constr.constr list
 val nLastDecls  : int -> goal sigma -> Context.Named.t
 
 val afterHyp    : Id.t -> goal sigma -> Context.Named.t
 
-val ifOnHyp     : (Id.t * EConstr.types -> bool) ->
+val ifOnHyp     : (Id.t * types -> bool) ->
                   (Id.t -> tactic) -> (Id.t -> tactic) ->
 		   Id.t -> tactic
 
@@ -99,9 +100,9 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic
 
 type branch_args = private {
   ity        : pinductive;  (** the type we were eliminating on *)
-  largs      : EConstr.constr list; (** its arguments *)
+  largs      : constr list; (** its arguments *)
   branchnum  : int;         (** the branch number *)
-  pred       : EConstr.constr;      (** the predicate we used *)
+  pred       : constr;      (** the predicate we used *)
   nassums    : int;         (** number of assumptions/letin to be introduced *)
   branchsign : bool list;   (** the signature of the branch.
                                 true=assumption, false=let-in *)
@@ -134,7 +135,7 @@ val elimination_sort_of_hyp  : Id.t -> goal sigma -> sorts_family
 val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family
 
 val pf_with_evars :  (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
-val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
+val pf_constr_of_global : Globnames.global_reference -> (Constr.constr -> tactic) -> tactic
 
 val elim_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic
 val case_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic
@@ -230,13 +231,13 @@ module New : sig
 
   val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t
 
-  val ifOnHyp     : (identifier * EConstr.types -> bool) ->
+  val ifOnHyp     : (identifier * types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
     identifier -> unit Proofview.tactic
 
   val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic
   val onLastHypId      : (identifier -> unit tactic) -> unit tactic
-  val onLastHyp        : (EConstr.constr -> unit tactic) -> unit tactic
+  val onLastHyp        : (constr -> unit tactic) -> unit tactic
   val onLastDecl       : (Context.Named.Declaration.t -> unit tactic) -> unit tactic
 
   val onHyps      : ([ `NF ], Context.Named.t) Proofview.Goal.enter ->
@@ -253,18 +254,18 @@ module New : sig
 
   val elimination_then :
     (branch_args -> unit Proofview.tactic) ->
-    EConstr.constr -> unit Proofview.tactic
+    constr -> unit Proofview.tactic
 
   val case_then_using :
     or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    EConstr.constr option -> pinductive -> EConstr.constr * EConstr.types -> unit Proofview.tactic
+    constr option -> pinductive -> constr * types -> unit Proofview.tactic
 
   val case_nodep_then_using :
     or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    EConstr.constr option -> pinductive -> EConstr.constr * EConstr.types -> unit Proofview.tactic
+    constr option -> pinductive -> constr * types -> unit Proofview.tactic
 
   val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
   val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
 
-  val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
+  val pf_constr_of_global : Globnames.global_reference -> (Constr.constr -> unit Proofview.tactic) -> unit Proofview.tactic
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f79f7f1a82..e4dd9eea26 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2821,7 +2821,6 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
   let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
-  let cl' = EConstr.of_constr cl' in
   let na = generalized_name sigma c t ids cl' na in
   let decl = match b with
     | None -> local_assum (na,t)