Tactics API using EConstr.

1 files changed, 5 insertions, 5 deletions

diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 3587ae2810..15b4e990d8 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -75,23 +75,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 * types
+val reduce_to_atomic_ind : env ->  evar_map -> EConstr.types -> pinductive * EConstr.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 * types
+val reduce_to_quantified_ind : env ->  evar_map -> EConstr.types -> pinductive * EConstr.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 -> types
+  env ->  evar_map -> global_reference -> EConstr.types -> EConstr.types
 
 val reduce_to_atomic_ref :
-  env ->  evar_map -> global_reference -> EConstr.types -> types
+  env ->  evar_map -> global_reference -> EConstr.types -> EConstr.types
 
 val find_hnf_rectype : 
-  env ->  evar_map -> EConstr.types -> pinductive * constr list
+  env ->  evar_map -> EConstr.types -> pinductive * EConstr.constr list
 
 val contextually : bool -> occurrences * constr_pattern ->
   (patvar_map -> reduction_function) -> reduction_function