diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 5242d0f3e..3031734fb 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -187,7 +187,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = compute_first_inversion_scheme env sigma ind sort dep_option in assert - (list_subset + (List.subset (global_vars env invGoal) (ids_of_named_context (named_context invEnv))); (* |