diff options
Diffstat (limited to 'test-suite/success/apply.v')
| -rw-r--r-- | test-suite/success/apply.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 8e829e061..d3c761019 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -97,13 +97,14 @@ Qed. (* Check use of unification of bindings types in specialize *) +Module Type Test. Variable P : nat -> Prop. Variable L : forall (l : nat), P l -> P l. Goal P 0 -> True. intros. specialize L with (1:=H). Abort. -Reset P. +End Test. (* Two examples that show that hnf_constr is used when unifying types of bindings (a simplification of a script from Field_Theory) *) |