diff options
Diffstat (limited to 'tactics/wcclausenv.mli')
| -rw-r--r-- | tactics/wcclausenv.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli index b1bf17e015..deae4091ff 100644 --- a/tactics/wcclausenv.mli +++ b/tactics/wcclausenv.mli @@ -5,6 +5,7 @@ open Names open Term open Sign +open Environ open Evd open Proof_trees open Tacmach @@ -27,11 +28,10 @@ type wc = walking_constraints val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv -(*i** -val add_prod_rel : 'a evar_map -> constr * context -> constr * context - -val add_prods_rel : 'a evar_map -> constr * context -> constr * context +val add_prod_rel : 'a evar_map -> constr * env -> constr * env +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 |