diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index e181c8e14..aaef0f072 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -12,7 +12,6 @@ open Util open Names open Term open Termops -open Context open Declarations open Tacmach open Clenv @@ -154,8 +153,8 @@ type branch_args = { branchnames : Tacexpr.intro_patterns} type branch_assumptions = { - ba : branch_args; (* the branch args *) - assums : named_context} (* the list of assumptions introduced *) + ba : branch_args; (* the branch args *) + assums : Context.Named.t} (* the list of assumptions introduced *) let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no |