Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions examples/AlmostFull.v
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ From Stdlib Require Import FunctionalExtensionality.
Set Equations Transparent.
Set Keyed Unification.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Local Set Firstorder Solver auto with arith core datatypes.

Ltac intuition_solver ::= auto with *.
Expand Down
1 change: 1 addition & 0 deletions test-suite/cfold.v
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ From Stdlib Require Import Bool.Bool.
Set Keyed Unification.
Set Implicit Arguments.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Inductive type : Set :=
| Nat : type
Expand Down
1 change: 1 addition & 0 deletions test-suite/issues/issue212.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ From Stdlib Require Import Lia ssreflect.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Import ListNotations.

Expand Down
1 change: 1 addition & 0 deletions test-suite/issues/issue349.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Set Implicit Arguments.

From Stdlib Require Import Lia Lists.List.
Expand Down
3 changes: 2 additions & 1 deletion test-suite/nestedobls.v
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
(**********************************************************************)

Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Set Implicit Arguments.
Unset Strict Implicit.
From Stdlib Require Import Arith.
Expand Down Expand Up @@ -39,4 +40,4 @@ Module Bug.
| exist _ k p'' := exist _ k _ } } }.
Proof. all:(clear test'; unfold MR; simpl; auto with arith). lia. Defined.

End Bug.
End Bug.
Loading