aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Cases.v1
-rw-r--r--test-suite/output/Coercions.v4
-rw-r--r--test-suite/output/Extraction_matchs_2413.v2
-rw-r--r--test-suite/output/Fixpoint.v2
-rw-r--r--test-suite/output/MExtraction.v63
-rw-r--r--test-suite/output/NoAxiomFromR.out1
-rw-r--r--test-suite/output/NoAxiomFromR.v10
-rw-r--r--test-suite/output/Notations3.v2
-rw-r--r--test-suite/output/PatternsInBinders.v2
-rw-r--r--test-suite/output/PrintInfos.out2
-rw-r--r--test-suite/output/Projections.v2
-rw-r--r--test-suite/output/Record.v4
-rw-r--r--test-suite/output/ShowMatch.v4
-rw-r--r--test-suite/output/UnivBinders.out18
-rw-r--r--test-suite/output/Warnings.v2
-rw-r--r--test-suite/output/auto.out16
-rw-r--r--test-suite/output/bug7191.out9
-rw-r--r--test-suite/output/bug7191.v3
-rw-r--r--test-suite/output/bug7348.out45
-rw-r--r--test-suite/output/bug7348.v25
-rw-r--r--test-suite/output/inference.v2
21 files changed, 181 insertions, 38 deletions
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4e949dcb04..a040b69b44 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -84,7 +84,6 @@ Print f.
(* Was enhancement request #5142 (error message reported on the most
general return clause heuristic) *)
-#[universes(template)]
Inductive gadt : Type -> Type :=
| gadtNat : nat -> gadt nat
| gadtTy : forall T, T -> gadt T.
diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v
index 6976f35a88..0e84bf3966 100644
--- a/test-suite/output/Coercions.v
+++ b/test-suite/output/Coercions.v
@@ -1,7 +1,7 @@
(* Submitted by Randy Pollack *)
-#[universes(template)] Record pred (S : Set) : Type := {sp_pred :> S -> Prop}.
-#[universes(template)] Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}.
+Record pred (S : Set) : Type := {sp_pred :> S -> Prop}.
+Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}.
Section testSection.
Variables (S : Set) (P : pred S) (R : rel S) (x : S).
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
index f9398fdca9..1ecd9771eb 100644
--- a/test-suite/output/Extraction_matchs_2413.v
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -101,7 +101,7 @@ Section decoder_result.
Variable inst : Type.
- #[universes(template)] Inductive decoder_result : Type :=
+ Inductive decoder_result : Type :=
| DecUndefined : decoder_result
| DecUnpredictable : decoder_result
| DecInst : inst -> decoder_result
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 9b25c2dbd3..61ae4edbd1 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
omega.
Qed.
-#[universes(template)] CoInductive Inf := S { projS : Inf }.
+CoInductive Inf := S { projS : Inf }.
Definition expand_Inf (x : Inf) := S (projS x).
CoFixpoint inf := S inf.
Eval compute in inf.
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index c0ef9b392d..668be1fdbc 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -1,14 +1,65 @@
-Require Import micromega.MExtraction.
-Require Import RingMicromega.
-Require Import QArith.
-Require Import VarMap.
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+(* *)
+(* Micromega: A reflexive tactic using the Positivstellensatz *)
+(* *)
+(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
+(* *)
+(************************************************************************)
+
+(* Used to generate micromega.ml *)
+
+Require Extraction.
Require Import ZMicromega.
Require Import QMicromega.
Require Import RMicromega.
+Require Import VarMap.
+Require Import RingMicromega.
+Require Import NArith.
+Require Import QArith.
+
+Extract Inductive prod => "( * )" [ "(,)" ].
+Extract Inductive list => list [ "[]" "(::)" ].
+Extract Inductive bool => bool [ true false ].
+Extract Inductive sumbool => bool [ true false ].
+Extract Inductive option => option [ Some None ].
+Extract Inductive sumor => option [ Some None ].
+(** Then, in a ternary alternative { }+{ }+{ },
+ - leftmost choice (Inleft Left) is (Some true),
+ - middle choice (Inleft Right) is (Some false),
+ - rightmost choice (Inright) is (None) *)
+
+
+(** To preserve its laziness, andb is normally expanded.
+ Let's rather use the ocaml && *)
+Extract Inlined Constant andb => "(&&)".
+
+Import Reals.Rdefinitions.
+
+Extract Constant R => "int".
+Extract Constant R0 => "0".
+Extract Constant R1 => "1".
+Extract Constant Rplus => "( + )".
+Extract Constant Rmult => "( * )".
+Extract Constant Ropp => "fun x -> - x".
+Extract Constant Rinv => "fun x -> 1 / x".
+(** In order to avoid annoying build dependencies the actual
+ extraction is only performed as a test in the test suite. *)
Recursive Extraction
-Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
- ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ
+ Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
+ Tauto.abst_form
+ ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ
List.map simpl_cone (*map_cone indexes*)
denorm Qpower vm_add
normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/test-suite/output/NoAxiomFromR.out b/test-suite/output/NoAxiomFromR.out
new file mode 100644
index 0000000000..7d7c521343
--- /dev/null
+++ b/test-suite/output/NoAxiomFromR.out
@@ -0,0 +1 @@
+Closed under the global context
diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v
new file mode 100644
index 0000000000..9cf6879699
--- /dev/null
+++ b/test-suite/output/NoAxiomFromR.v
@@ -0,0 +1,10 @@
+Require Import Psatz.
+
+Inductive TT : Set :=
+| C : nat -> TT.
+
+Lemma lem4 : forall (n m : nat),
+S m <= m -> C (S m) <> C n -> False.
+Proof. firstorder. Qed.
+
+Print Assumptions lem4.
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 29614c032a..aeebc0f98b 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
(**********************************************************************)
(* Test printing of #4932 *)
-#[universes(template)] Inductive ftele : Type :=
+Inductive ftele : Type :=
| fb {T:Type} : T -> ftele
| fr {T} : (T -> ftele) -> ftele.
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 0c1b08f5a3..d671053c07 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -53,7 +53,7 @@ Module Suboptimal.
(** This test shows an example which exposes the [let] introduced by
the pattern notation in binders. *)
-#[universes(template)] Inductive Fin (n:nat) := Z : Fin n.
+Inductive Fin (n:nat) := Z : Fin n.
Definition F '(n,p) : Type := (Fin n * Fin p)%type.
Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
Print both_z.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ab4172711e..e788977fb7 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,6 +1,6 @@
existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
-existT is template universe polymorphic
+existT is template universe polymorphic on sigT.u0 sigT.u1
Argument A is implicit
Argument scopes are [type_scope function_scope _ _]
Expands to: Constructor Coq.Init.Specif.existT
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
index 35f36e87d7..14d63d39c4 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -6,7 +6,7 @@ Class HostFunction := host_func : Type.
Section store.
Context `{HostFunction}.
- #[universes(template)] Record store := { store_funcs : host_func }.
+ Record store := { store_funcs : host_func }.
End store.
Check (fun (S:@store nat) => S.(store_funcs)).
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 4fe7b051f8..d9a649fadc 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -20,12 +20,12 @@ Check {| field := 5 |}.
Check build_r 5.
Check build_c 5.
-#[universes(template)] Record N := C { T : Type; _ : True }.
+Record N := C { T : Type; _ : True }.
Check fun x:N => let 'C _ p := x in p.
Check fun x:N => let 'C T _ := x in T.
Check fun x:N => let 'C T p := x in (T,p).
-#[universes(template)] Record M := D { U : Type; a := 0; q : True }.
+Record M := D { U : Type; a := 0; q : True }.
Check fun x:M => let 'D T _ p := x in p.
Check fun x:M => let 'D T _ p := x in T.
Check fun x:M => let 'D T p := x in (T,p).
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v
index 99183f2064..9cf6ad35b8 100644
--- a/test-suite/output/ShowMatch.v
+++ b/test-suite/output/ShowMatch.v
@@ -3,12 +3,12 @@
*)
Module A.
- #[universes(template)] Inductive foo := f.
+ Inductive foo := f.
Show Match foo. (* no need to disambiguate *)
End A.
Module B.
- #[universes(template)] Inductive foo := f.
+ Inductive foo := f.
(* local foo shadows A.foo, so constructor "f" needs disambiguation *)
Show Match A.foo.
End B.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 222a808768..a89fd64999 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -68,9 +68,9 @@ mono
The command has indeed failed with message:
Universe u already exists.
bobmorane =
-let tt := Type@{UnivBinders.32} in
-let ff := Type@{UnivBinders.34} in tt -> ff
- : Type@{max(UnivBinders.31,UnivBinders.33)}
+let tt := Type@{UnivBinders.33} in
+let ff := Type@{UnivBinders.35} in tt -> ff
+ : Type@{max(UnivBinders.32,UnivBinders.34)}
The command has indeed failed with message:
Universe u already bound.
foo@{E M N} =
@@ -143,16 +143,16 @@ Applied.infunct@{u v} =
inmod@{u} -> Type@{v}
: Type@{max(u+1,v+1)}
(* u v |= *)
-axfoo@{i UnivBinders.56 UnivBinders.57} :
-Type@{UnivBinders.56} -> Type@{i}
-(* i UnivBinders.56 UnivBinders.57 |= *)
+axfoo@{i UnivBinders.57 UnivBinders.58} :
+Type@{UnivBinders.57} -> Type@{i}
+(* i UnivBinders.57 UnivBinders.58 |= *)
axfoo is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.56 UnivBinders.57} :
-Type@{UnivBinders.57} -> Type@{i}
-(* i UnivBinders.56 UnivBinders.57 |= *)
+axbar@{i UnivBinders.57 UnivBinders.58} :
+Type@{UnivBinders.58} -> Type@{i}
+(* i UnivBinders.57 UnivBinders.58 |= *)
axbar is universe polymorphic
Argument scope is [type_scope]
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
index 0eb5db1733..7465442cab 100644
--- a/test-suite/output/Warnings.v
+++ b/test-suite/output/Warnings.v
@@ -1,5 +1,5 @@
(* Term in warning was not printed in the right environment at some time *)
-#[universes(template)] Record A := { B:Type; b:B->B }.
+Record A := { B:Type; b:B->B }.
Definition a B := {| B:=B; b:=fun x => x |}.
Canonical Structure a.
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
index 2761b87b02..5e81b43504 100644
--- a/test-suite/output/auto.out
+++ b/test-suite/output/auto.out
@@ -2,18 +2,18 @@
simple apply or_intror (in core).
intro.
assumption.
-Debug: (* debug auto: *)
-Debug: * assumption. (*fail*)
-Debug: * intro. (*fail*)
-Debug: * simple apply or_intror (in core). (*success*)
-Debug: ** assumption. (*fail*)
-Debug: ** intro. (*success*)
-Debug: ** assumption. (*success*)
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+* simple apply or_intror (in core). (*success*)
+** assumption. (*fail*)
+** intro. (*success*)
+** assumption. (*success*)
(* info eauto: *)
simple apply or_intror.
intro.
exact H.
-Debug: (* debug eauto: *)
+(* debug eauto: *)
Debug: 1 depth=5
Debug: 1.1 depth=4 simple apply or_intror
Debug: 1.1.1 depth=4 intro
diff --git a/test-suite/output/bug7191.out b/test-suite/output/bug7191.out
new file mode 100644
index 0000000000..005455e30c
--- /dev/null
+++ b/test-suite/output/bug7191.out
@@ -0,0 +1,9 @@
+
+type unit0 =
+| Tt
+
+(** val f : unit0 -> unit0 **)
+
+let f _ =
+ assert false (* absurd case *)
+
diff --git a/test-suite/output/bug7191.v b/test-suite/output/bug7191.v
new file mode 100644
index 0000000000..1aa4625b6c
--- /dev/null
+++ b/test-suite/output/bug7191.v
@@ -0,0 +1,3 @@
+Require Extraction.
+Definition f (x : False) : unit -> unit := match x with end.
+Recursive Extraction f.
diff --git a/test-suite/output/bug7348.out b/test-suite/output/bug7348.out
new file mode 100644
index 0000000000..325ee95ae2
--- /dev/null
+++ b/test-suite/output/bug7348.out
@@ -0,0 +1,45 @@
+Extracted code successfully compiled
+
+type __ = Obj.t
+
+type unit0 =
+| Tt
+
+type bool =
+| True
+| False
+
+module Case1 =
+ struct
+ type coq_rec = { f : bool }
+
+ (** val f : bool -> coq_rec -> bool **)
+
+ let f _ r =
+ r.f
+
+ (** val silly : bool -> coq_rec -> __ **)
+
+ let silly x b =
+ match x with
+ | True -> Obj.magic b.f
+ | False -> Obj.magic Tt
+ end
+
+module Case2 =
+ struct
+ type coq_rec = { f : (bool -> bool) }
+
+ (** val f : bool -> coq_rec -> bool -> bool **)
+
+ let f _ r =
+ r.f
+
+ (** val silly : bool -> coq_rec -> __ **)
+
+ let silly x b =
+ match x with
+ | True -> Obj.magic b.f False
+ | False -> Obj.magic Tt
+ end
+
diff --git a/test-suite/output/bug7348.v b/test-suite/output/bug7348.v
new file mode 100644
index 0000000000..782b27ce96
--- /dev/null
+++ b/test-suite/output/bug7348.v
@@ -0,0 +1,25 @@
+Require Extraction.
+
+Extraction Language OCaml.
+Set Extraction KeepSingleton.
+
+Module Case1.
+
+Record rec (x : bool) := { f : bool }.
+
+Definition silly x (b : rec x) :=
+ if x return (if x then bool else unit) then f x b else tt.
+
+End Case1.
+
+Module Case2.
+
+Record rec (x : bool) := { f : bool -> bool }.
+
+Definition silly x (b : rec x) :=
+ if x return (if x then bool else unit) then f x b false else tt.
+
+End Case2.
+
+Extraction TestCompile Case1.silly Case2.silly.
+Recursive Extraction Case1.silly Case2.silly.
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 209fedc343..57a4739e9f 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -21,6 +21,6 @@ Print P.
(* Note: exact numbers of evars are not important... *)
-#[universes(template)] Inductive T (n:nat) : Type := A : T n.
+Inductive T (n:nat) : Type := A : T n.
Check fun n (y:=A n:T n) => _ _ : T n.
Check fun n => _ _ : T n.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 22:41:58 +0000