diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ca22b899b7..d20712b5d3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -153,7 +153,7 @@ let dyn_mutual_cofix argsl gl = (* Reduction and conversion tactics *) (**************************************************************) -type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr +type tactic_reduction = env -> evar_map -> constr -> constr (* The following two tactics apply an arbitrary reduction function either to the conclusion or to a |