aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/wcclausenv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/wcclausenv.mli')
-rw-r--r--tactics/wcclausenv.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index af96177b3..b3d372f21 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -33,10 +33,10 @@ val add_prods_rel : 'a evar_map -> constr * env -> constr * env
(*i**
val add_prod_sign :
- 'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+ 'a evar_map -> constr * types signature -> constr * types signature
val add_prods_sign :
- 'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+ 'a evar_map -> constr * types signature -> constr * types signature
**i*)
val res_pf_THEN :