Merge remote-tracking branch 'forge/v8.5'

2 files changed, 257 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v
new file mode 100644
index 000000000..4f29b76c6
--- /dev/null
+++ b/test-suite/bugs/closed/3446.v
@@ -0,0 +1,47 @@
+(* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *)
+(* Set Asymmetric Patterns. *)
+(* Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). *)
+(* Notation "A -> B" := (forall (_ : A), B). *)
+
+(* Notation "x → y" := (x -> y) *)
+(*   (at level 99, y at level 200, right associativity): type_scope. *)
+(* Record sigT A (P : A -> Type) := *)
+(*   { projT1 : A ; projT2 : P projT1 }. *)
+(* Arguments projT1 {A P} s. *)
+(* Arguments projT2 {A P} s. *)
+(* Set Universe Polymorphism. *)
+(* Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). *)
+(* Reserved Notation "x = y" (at level 70, no associativity). *)
+(* Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). *)
+(* Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. *)
+(* Reserved Notation "{ x : A  & P }" (at level 0, x at level 99). *)
+(* Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope. *)
+
+
+(* Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v. *)
+(* Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). *)
+
+(* Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := *)
+(*   @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). *)
+
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+Arguments projT1 {_ _} _.
+Notation "( x ; y )" := (existT _ x y).
+Notation pr1 := projT1.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3).
+Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT P) (pq : {p : u.1 = v.1 &  p # u.2 = v.2}), u = v.
+Instance isequiv_pr1_contr {A} {P : A -> Type} : IsEquiv (@pr1 A P) | 100.
+Admitted.
+
+Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT P) : u.1 = v.1 -> u = v := 
+  path_sigma_uncurried P u v o pr1^-1.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4057.v b/test-suite/bugs/closed/4057.v
new file mode 100644
index 000000000..4f0e696c9
--- /dev/null
+++ b/test-suite/bugs/closed/4057.v
@@ -0,0 +1,210 @@
+Require Coq.Strings.String.
+
+Set Implicit Arguments.
+
+Axiom falso : False.
+Ltac admit := destruct falso.
+
+Reserved Notation "[ x ]".
+
+Record string_like (CharType : Type) :=
+  {
+    String :> Type;
+    Singleton : CharType -> String where "[ x ]" := (Singleton x);
+    Empty : String;
+    Concat : String -> String -> String where "x ++ y" := (Concat x y);
+    bool_eq : String -> String -> bool;
+    bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y;
+    Length : String -> nat
+  }.
+
+Delimit Scope string_like_scope with string_like.
+Bind Scope string_like_scope with String.
+Arguments Length {_%type_scope _} _%string_like.
+Infix "++" := (@Concat _ _) : string_like_scope.
+
+Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String)
+  := Length s1 < Length s2 \/ s1 = s2.
+Infix "≤s" := str_le (at level 70, right associativity).
+
+Module Export ContextFreeGrammar.
+  Import Coq.Strings.String.
+  Import Coq.Lists.List.
+
+  Section cfg.
+    Variable CharType : Type.
+
+    Section definitions.
+
+      Inductive item :=
+    | NonTerminal (name : string).
+
+      Definition production := list item.
+      Definition productions := list production.
+
+      Record grammar :=
+        {
+          Start_symbol :> string;
+          Lookup :> string -> productions
+        }.
+    End definitions.
+
+    Section parse.
+      Variable String : string_like CharType.
+      Variable G : grammar.
+
+      Inductive parse_of : String -> productions -> Type :=
+      | ParseHead : forall str pat pats, parse_of_production str pat
+                                         -> parse_of str (pat::pats)
+      | ParseTail : forall str pat pats, parse_of str pats
+                                         -> parse_of str (pat::pats)
+      with parse_of_production : String -> production -> Type :=
+      | ParseProductionCons : forall str pat strs pats,
+                                parse_of_item str pat
+                                -> parse_of_production strs pats
+                                -> parse_of_production (str ++ strs) (pat::pats)
+      with parse_of_item : String -> item -> Type :=
+      | ParseNonTerminal : forall name str, parse_of str (Lookup G name)
+                                            -> parse_of_item str (NonTerminal 
+name).
+    End parse.
+  End cfg.
+
+End ContextFreeGrammar.
+Module Export ContextFreeGrammarProperties.
+
+  Section cfg.
+    Context CharType (String : string_like CharType) (G : grammar)
+            (P : String.string -> Type).
+
+    Fixpoint Forall_parse_of {str pats} (p : parse_of String G str pats)
+      := match p with
+           | @ParseHead _ _ _ str pat pats p'
+             => Forall_parse_of_production p'
+           | @ParseTail _ _ _ _ _ _ p'
+             => Forall_parse_of p'
+         end
+    with Forall_parse_of_production {str pat} (p : parse_of_production String G 
+str pat)
+         := let Forall_parse_of_item {str it} (p : parse_of_item String G str 
+it)
+                := match p return Type with
+                     | @ParseNonTerminal _ _ _ name str p'
+                       => (P name * Forall_parse_of p')%type
+                   end in
+            match p return Type with
+              | @ParseProductionCons _ _ _ str pat strs pats p' p''
+                => (Forall_parse_of_item p' * Forall_parse_of_production 
+p'')%type
+            end.
+
+    Definition Forall_parse_of_item {str it} (p : parse_of_item String G str it)
+      := match p return Type with
+           | @ParseNonTerminal _ _ _ name str p'
+             => (P name * Forall_parse_of p')%type
+         end.
+  End cfg.
+
+End ContextFreeGrammarProperties.
+
+Module Export DependentlyTyped.
+  Import Coq.Strings.String.
+
+  Section recursive_descent_parser.
+
+    Class parser_computational_predataT :=
+      { nonterminal_names_listT : Type;
+        initial_nonterminal_names_data : nonterminal_names_listT;
+        is_valid_nonterminal_name : nonterminal_names_listT -> string -> bool;
+        remove_nonterminal_name : nonterminal_names_listT -> string -> 
+nonterminal_names_listT }.
+
+  End recursive_descent_parser.
+
+End DependentlyTyped.
+Import Coq.Strings.String.
+Import Coq.Lists.List.
+
+Section cfg.
+  Context CharType (String : string_like CharType) (G : grammar).
+  Context (names_listT : Type)
+          (initial_names_data : names_listT)
+          (is_valid_name : names_listT -> string -> bool)
+          (remove_name : names_listT -> string -> names_listT).
+
+  Inductive minimal_parse_of
+  : forall (str0 : String) (valid : names_listT)
+           (str : String),
+      productions -> Type :=
+  | MinParseHead : forall str0 valid str pat pats,
+                     @minimal_parse_of_production str0 valid str pat
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  | MinParseTail : forall str0 valid str pat pats,
+                     @minimal_parse_of str0 valid str pats
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  with minimal_parse_of_production
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           production -> Type :=
+  | MinParseProductionNil : forall str0 valid,
+                              @minimal_parse_of_production str0 valid (Empty _) 
+nil
+  | MinParseProductionCons : forall str0 valid str strs pat pats,
+                               str ++ strs ≤s str0
+                               -> @minimal_parse_of_item str0 valid str pat
+                               -> @minimal_parse_of_production str0 valid strs 
+pats
+                               -> @minimal_parse_of_production str0 valid (str 
+++ strs) (pat::pats)
+  with minimal_parse_of_item
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           item -> Type :=
+  | MinParseNonTerminal
+    : forall str0 valid str name,
+        @minimal_parse_of_name str0 valid str name
+        -> @minimal_parse_of_item str0 valid str (NonTerminal name)
+  with minimal_parse_of_name
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           string -> Type :=
+  | MinParseNonTerminalStrLt
+    : forall str0 valid name str,
+        @minimal_parse_of str initial_names_data str (Lookup G name)
+        -> @minimal_parse_of_name str0 valid str name
+  | MinParseNonTerminalStrEq
+    : forall str valid name,
+        @minimal_parse_of str (remove_name valid name) str (Lookup G name)
+        -> @minimal_parse_of_name str valid str name.
+  Definition parse_of_item_name__of__minimal_parse_of_name
+  : forall {str0 valid str name} (p : @minimal_parse_of_name str0 valid str 
+name),
+      parse_of_item String G str (NonTerminal name).
+  Proof.
+    admit.
+  Defined.
+
+End cfg.
+
+Section recursive_descent_parser.
+  Context (CharType : Type)
+          (String : string_like CharType)
+          (G : grammar).
+  Context {premethods : parser_computational_predataT}.
+  Let P : string -> Prop.
+  Proof.
+    admit.
+  Defined.
+
+  Let mp_parse_nonterminal_name str0 valid str nonterminal_name
+    := { p' : minimal_parse_of_name String G initial_nonterminal_names_data 
+remove_nonterminal_name str0 valid str nonterminal_name & Forall_parse_of_item 
+P (parse_of_item_name__of__minimal_parse_of_name p') }.
+
+  Goal False.
+  Proof.
+    clear -mp_parse_nonterminal_name.
+    subst P.
+    simpl in *.
+    admit.
+  Qed.