diff options
Diffstat (limited to 'test-suite/bugs/closed/2775.v')
| -rw-r--r-- | test-suite/bugs/closed/2775.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2775.v b/test-suite/bugs/closed/2775.v new file mode 100644 index 00000000..f1f384bd --- /dev/null +++ b/test-suite/bugs/closed/2775.v @@ -0,0 +1,6 @@ +Inductive typ : forall (T:Type), list T -> Type -> Prop := + | Get : forall (T:Type) (l:list T), typ T l T. + + +Derive Inversion inv with +(forall (X: Type) (y: list nat), typ nat y X) Sort Prop. |