diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Match_subterm.out | 8 | ||||
| -rw-r--r-- | test-suite/output/Match_subterm.v | 6 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 5 |
3 files changed, 14 insertions, 5 deletions
diff --git a/test-suite/output/Match_subterm.out b/test-suite/output/Match_subterm.out new file mode 100644 index 000000000..951a98db0 --- /dev/null +++ b/test-suite/output/Match_subterm.out @@ -0,0 +1,8 @@ +(0 = 1) +eq +nat +0 +1 +S +0 +2 diff --git a/test-suite/output/Match_subterm.v b/test-suite/output/Match_subterm.v new file mode 100644 index 000000000..2c44b1879 --- /dev/null +++ b/test-suite/output/Match_subterm.v @@ -0,0 +1,6 @@ +Goal 0 = 1. +match goal with +| |- context [?v] => + idtac v ; fail +| _ => idtac 2 +end. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 3bc9c7f9e..082cbfbe1 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -198,11 +198,6 @@ Goal forall x : nat, F1 x -> G1 x. refine (fun x H => proj2 (_ x H) _). Abort. -(* First-order unification between beta-redex (is it useful ?) *) - -Check fun (y: (forall x:((fun y:Type => bool) nat), True)) - (z: (fun z:Type => bool) _) => y z. - (* Remark: the following example does not succeed any longer in 8.2 because, the algorithm is more general and does exclude a solution that it should exclude for typing reason. Handling of types and backtracking is still to |