diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/output/Extraction_matchs_2413.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/output/Extraction_matchs_2413.v')
-rw-r--r-- | test-suite/output/Extraction_matchs_2413.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index f5610efc..6c514b16 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -22,8 +22,8 @@ Inductive hole (A:Set) : Set := Hole | Hole2. Definition wrong_id (A B : Set) (x:hole A) : hole B := match x with - | Hole => @Hole _ - | Hole2 => @Hole2 _ + | Hole _ => @Hole _ + | Hole2 _ => @Hole2 _ end. Extraction wrong_id. (** should _not_ be optimized as an identity *) @@ -114,9 +114,9 @@ Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode) | Some oc => match f w with | DecInst i => DecInst (g i oc) - | DecError m => @DecError inst m - | DecUndefined => @DecUndefined inst - | DecUnpredictable => @DecUnpredictable inst + | DecError _ m => @DecError inst m + | DecUndefined _ => @DecUndefined inst + | DecUnpredictable _ => @DecUnpredictable inst end | None => @DecUndefined inst end. |