Imported Upstream version 8.3pl1upstream/8.3pl1

4 files changed, 181 insertions, 7 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 62d443d0..98bab43b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -40,7 +40,7 @@ endif
 
 command := $(coqtop) -top Top -load-vernac-source
 coqc := $(coqtop) -compile
-coqdep := $(BIN)coqdep
+coqdep := $(BIN)coqdep -coqlib $(LIB)
 
 SHOW := $(if $(VERBOSE),@true,@echo)
 HIDE := $(if $(VERBOSE),,@)
diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v
index c7926711..8cc43ee6 100644
--- a/test-suite/bugs/closed/shouldsucceed/2388.v
+++ b/test-suite/bugs/closed/shouldsucceed/2388.v
@@ -2,9 +2,3 @@
 
 Fail Parameters (A:Prop) (a:A A).
 
-(* This is a variant (reported as part of bug #2347) *)
-
-Require Import EquivDec.                                              
-Fail Program Instance bool_eq_eqdec : EqDec bool eq := 
-   {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
-
diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out
new file mode 100644
index 00000000..7bce6671
--- /dev/null
+++ b/test-suite/output/Extraction_matchs_2413.out
@@ -0,0 +1,52 @@
+(** val test1 : bool -> bool **)
+
+let test1 b =
+  b
+(** val test2 : bool -> bool **)
+
+let test2 b =
+  False
+(** val wrong_id : 'a1 hole -> 'a2 hole **)
+
+let wrong_id = function
+  | Hole -> Hole
+  | Hole2 -> Hole2
+(** val test3 : 'a1 option -> 'a1 option **)
+
+let test3 o =
+  o
+(** val test4 : indu -> indu **)
+
+let test4 = function
+  | A m -> A (S m)
+  | x -> x
+(** val test5 : indu -> indu **)
+
+let test5 = function
+  | A m -> A (S m)
+  | _ -> B
+(** val test6 : indu' -> indu' **)
+
+let test6 = function
+  | A' m -> A' (S m)
+  | E' -> B'
+  | F' -> B'
+  | _ -> C'
+(** val test7 : indu -> nat option **)
+
+let test7 = function
+  | A m -> Some m
+  | _ -> None
+(** val decode_cond_mode :
+    (word -> opcode option) -> (word -> 'a1 decoder_result) -> word -> ('a1
+    -> opcode -> 'a2) -> 'a2 decoder_result **)
+
+let decode_cond_mode condition f w g =
+  match condition w with
+    | Some oc ->
+        (match f w with
+           | DecUndefined -> DecUndefined
+           | DecUnpredictable -> DecUnpredictable
+           | DecInst i -> DecInst (g i oc)
+           | DecError m -> DecError m)
+    | None -> DecUndefined
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
new file mode 100644
index 00000000..f5610efc
--- /dev/null
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -0,0 +1,128 @@
+(** Extraction : tests of optimizations of pattern matching *)
+
+(** First, a few basic tests *)
+
+Definition test1 b :=
+ match b with
+   | true => true
+   | false => false
+ end.
+
+Extraction test1. (** should be seen as the identity *)
+
+Definition test2 b :=
+ match b with
+   | true => false
+   | false => false
+ end.
+
+Extraction test2. (** should be seen a the always-false constant function *)
+
+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 _
+ end.
+
+Extraction wrong_id. (** should _not_ be optimized as an identity *)
+
+Definition test3 (A:Type)(o : option A) :=
+ match o with
+   | Some x => Some x
+   | None  => None
+ end.
+
+Extraction test3.  (** Even with type parameters, should be seen as identity *)
+
+Inductive indu : Type := A : nat -> indu | B | C.
+
+Definition test4 n :=
+ match n with
+   | A m => A (S m)
+   | B => B
+   | C => C
+ end.
+
+Extraction test4. (** should merge branchs B C into a x->x *)
+
+Definition test5 n :=
+ match n with
+   | A m => A (S m)
+   | B => B
+   | C => B
+ end.
+
+Extraction test5. (** should merge branches B C into _->B *)
+
+Inductive indu' : Type := A' : nat -> indu' | B' | C' | D' | E' | F'.
+
+Definition test6 n :=
+ match n with
+   | A' m => A' (S m)
+   | B' => C'
+   | C' => C'
+   | D' => C'
+   | E' => B'
+   | F' => B'
+ end.
+
+Extraction test6. (** should merge some branches into a _->C' *)
+
+(** NB : In Coq, "| a => a"  corresponds to n, hence some "| _ -> n" are
+    extracted *)
+
+Definition test7 n :=
+  match n with
+    | A m => Some m
+    | B => None
+    | C => None
+  end.
+
+Extraction test7. (** should merge branches B,C into a _->None *)
+
+(** Script from bug #2413 *)
+
+Set Implicit Arguments.
+
+Section S.
+
+Definition message := nat.
+Definition word := nat.
+Definition mode := nat.
+Definition opcode := nat.
+
+Variable condition : word -> option opcode.
+
+Section decoder_result.
+
+ Variable inst : Type.
+
+ Inductive decoder_result : Type :=
+ | DecUndefined : decoder_result
+ | DecUnpredictable : decoder_result
+ | DecInst : inst -> decoder_result
+ | DecError : message -> decoder_result.
+
+End decoder_result.
+
+Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode)
+  (w : word) (inst : Type) (g : mode -> opcode -> inst) :
+  decoder_result inst :=
+  match condition w with
+    | Some oc =>
+      match f w with
+        | DecInst i => DecInst (g i oc)
+        | DecError m => @DecError inst m
+        | DecUndefined => @DecUndefined inst
+        | DecUnpredictable => @DecUnpredictable inst
+      end
+    | None => @DecUndefined inst
+  end.
+
+End S.
+
+Extraction decode_cond_mode.
+(** inner match should not be factorized with a partial x->x (different type) *)
+