aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/FSets/FMapAVL.v8
-rw-r--r--theories/Init/Notations.v35
-rw-r--r--theories/Init/Specif.v29
-rw-r--r--theories/PArith/BinPos.v2
-rw-r--r--theories/dune38
-rw-r--r--theories/micromega/Lia.v2
-rw-r--r--theories/micromega/Lqa.v2
-rw-r--r--theories/micromega/Lra.v2
-rw-r--r--theories/setoid_ring/Field_tac.v4
9 files changed, 85 insertions, 37 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 82055c4752..f78c0ecc1e 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -550,14 +550,14 @@ Ltac intuition_in := repeat (intuition; inv In; inv MapsTo).
Let's do its job by hand: *)
Ltac join_tac :=
- intros l; induction l as [| ll _ lx ld lr Hlr lh];
- [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join;
- [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE];
+ intros ?l; induction l as [| ?ll _ ?lx ?ld ?lr ?Hlr ?lh];
+ [ | intros ?x ?d ?r; induction r as [| ?rl ?Hrl ?rx ?rd ?rr _ ?rh]; unfold join;
+ [ | destruct (gt_le_dec lh (rh+2)) as [?GT|?LE];
[ match goal with |- context [ bal ?u ?v ?w ?z ] =>
replace (bal u v w z)
with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
end
- | destruct (gt_le_dec rh (lh+2)) as [GT'|LE'];
+ | destruct (gt_le_dec rh (lh+2)) as [?GT'|?LE'];
[ match goal with |- context [ bal ?u ?v ?w ?z ] =>
replace (bal u v w z)
with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto]
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index fdb88a0c82..a5e4178b93 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -68,33 +68,40 @@ Reserved Notation "{ x }" (at level 0, x at level 99).
(** Notations for sigma-types or subsets *)
-Reserved Notation "{ A } + { B }" (at level 50, left associativity).
-Reserved Notation "A + { B }" (at level 50, left associativity).
+Reserved Notation "{ A } + { B }" (at level 50, left associativity).
+Reserved Notation "A + { B }" (at level 50, left associativity).
-Reserved Notation "{ x | P }" (at level 0, x at level 99).
-Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x | P }" (at level 0, x at level 99).
+Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
-Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
-Reserved Notation "{ x & P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x & P }" (at level 0, x at level 99).
+Reserved Notation "{ x & P & Q }" (at level 0, x at level 99).
+
+Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
Reserved Notation "{ ' pat | P }"
- (at level 0, pat strict pattern, format "{ ' pat | P }").
+ (at level 0, pat strict pattern, format "{ ' pat | P }").
Reserved Notation "{ ' pat | P & Q }"
- (at level 0, pat strict pattern, format "{ ' pat | P & Q }").
+ (at level 0, pat strict pattern, format "{ ' pat | P & Q }").
Reserved Notation "{ ' pat : A | P }"
(at level 0, pat strict pattern, format "{ ' pat : A | P }").
Reserved Notation "{ ' pat : A | P & Q }"
- (at level 0, pat strict pattern, format "{ ' pat : A | P & Q }").
+ (at level 0, pat strict pattern, format "{ ' pat : A | P & Q }").
+
+Reserved Notation "{ ' pat & P }"
+ (at level 0, pat strict pattern, format "{ ' pat & P }").
+Reserved Notation "{ ' pat & P & Q }"
+ (at level 0, pat strict pattern, format "{ ' pat & P & Q }").
Reserved Notation "{ ' pat : A & P }"
- (at level 0, pat strict pattern, format "{ ' pat : A & P }").
+ (at level 0, pat strict pattern, format "{ ' pat : A & P }").
Reserved Notation "{ ' pat : A & P & Q }"
- (at level 0, pat strict pattern, format "{ ' pat : A & P & Q }").
+ (at level 0, pat strict pattern, format "{ ' pat : A & P & Q }").
(** Support for Gonthier-Ssreflect's "if c is pat then u else v" *)
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 692fe3d8d0..59ee252d35 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -58,23 +58,26 @@ Arguments sig2 (A P Q)%type.
Arguments sigT (A P)%type.
Arguments sigT2 (A P Q)%type.
-Notation "{ x | P }" := (sig (fun x => P)) : type_scope.
-Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
-Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope.
-Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) :
+Notation "{ x | P }" := (sig (fun x => P)) : type_scope.
+Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
+Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope.
+Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) :
type_scope.
-Notation "{ x & P }" := (sigT (fun x => P)) : type_scope.
-Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
-Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) :
+Notation "{ x & P }" := (sigT (fun x => P)) : type_scope.
+Notation "{ x & P & Q }" := (sigT2 (fun x => P) (fun x => Q)) : type_scope.
+Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
+Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) :
type_scope.
-Notation "{ ' pat | P }" := (sig (fun pat => P)) : type_scope.
-Notation "{ ' pat | P & Q }" := (sig2 (fun pat => P) (fun pat => Q)) : type_scope.
-Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P)) : type_scope.
-Notation "{ ' pat : A | P & Q }" := (sig2 (A:=A) (fun pat => P) (fun pat => Q)) :
+Notation "{ ' pat | P }" := (sig (fun pat => P)) : type_scope.
+Notation "{ ' pat | P & Q }" := (sig2 (fun pat => P) (fun pat => Q)) : type_scope.
+Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P)) : type_scope.
+Notation "{ ' pat : A | P & Q }" := (sig2 (A:=A) (fun pat => P) (fun pat => Q)) :
type_scope.
-Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope.
-Notation "{ ' pat : A & P & Q }" := (sigT2 (A:=A) (fun pat => P) (fun pat => Q)) :
+Notation "{ ' pat & P }" := (sigT (fun pat => P)) : type_scope.
+Notation "{ ' pat & P & Q }" := (sigT2 (fun pat => P) (fun pat => Q)) : type_scope.
+Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope.
+Notation "{ ' pat : A & P & Q }" := (sigT2 (A:=A) (fun pat => P) (fun pat => Q)) :
type_scope.
Add Printing Let sig.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 387ab75362..4179765dca 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1753,7 +1753,7 @@ Qed.
Ltac destr_pggcdn IHn :=
match goal with |- context [ ggcdn _ ?x ?y ] =>
- generalize (IHn x y); destruct ggcdn as (g,(u,v)); simpl
+ generalize (IHn x y); destruct ggcdn as (?g,(?u,?v)); simpl
end.
Lemma ggcdn_correct_divisors : forall n a b,
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000000..b9af76d699
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,38 @@
+(coq.theory
+ (name Coq)
+ (package coq)
+ (synopsis "Coq's Standard Library")
+ (flags -q)
+ ; (mode native)
+ (boot)
+ ; (per_file
+ ; (Init/*.v -> -boot))
+ (libraries
+ coq.plugins.ltac
+ coq.plugins.tauto
+
+ coq.plugins.cc
+ coq.plugins.firstorder
+
+ coq.plugins.numeral_notation
+ coq.plugins.string_notation
+ coq.plugins.int63_syntax
+ coq.plugins.r_syntax
+ coq.plugins.float_syntax
+
+ coq.plugins.btauto
+ coq.plugins.rtauto
+
+ coq.plugins.setoid_ring
+ coq.plugins.nsatz
+ coq.plugins.omega
+
+ coq.plugins.zify
+ coq.plugins.micromega
+
+ coq.plugins.funind
+
+ coq.plugins.ssreflect
+ coq.plugins.derive))
+
+(include_subdirs qualified)
diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v
index f3b70f61d2..3d955fec4f 100644
--- a/theories/micromega/Lia.v
+++ b/theories/micromega/Lia.v
@@ -21,7 +21,7 @@ Declare ML Module "micromega_plugin".
Ltac zchecker :=
- intros __wit __varmap __ff ;
+ intros ?__wit ?__varmap ?__ff ;
exact (ZTautoChecker_sound __ff __wit
(@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true)
(@find Z Z0 __varmap)).
diff --git a/theories/micromega/Lqa.v b/theories/micromega/Lqa.v
index 786c9275f0..8a4d59b1bd 100644
--- a/theories/micromega/Lqa.v
+++ b/theories/micromega/Lqa.v
@@ -23,7 +23,7 @@ Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
Ltac rchange :=
- intros __wit __varmap __ff ;
+ intros ?__wit ?__varmap ?__ff ;
change (Tauto.eval_bf (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
apply (QTautoChecker_sound __ff __wit).
diff --git a/theories/micromega/Lra.v b/theories/micromega/Lra.v
index 3ac4772ba4..22cef50e0d 100644
--- a/theories/micromega/Lra.v
+++ b/theories/micromega/Lra.v
@@ -23,7 +23,7 @@ Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
Ltac rchange :=
- intros __wit __varmap __ff ;
+ intros ?__wit ?__varmap ?__ff ;
change (Tauto.eval_bf (Reval_formula (@find R 0%R __varmap)) __ff) ;
apply (RTautoChecker_sound __ff __wit).
diff --git a/theories/setoid_ring/Field_tac.v b/theories/setoid_ring/Field_tac.v
index 89a5ca6740..15b2618e47 100644
--- a/theories/setoid_ring/Field_tac.v
+++ b/theories/setoid_ring/Field_tac.v
@@ -215,7 +215,7 @@ Ltac fold_field_cond req :=
Ltac simpl_PCond FLD :=
let req := get_FldEq FLD in
let lemma := get_CondLemma FLD in
- try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
+ try (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
protect_fv "field_cond";
fold_field_cond req;
try exact I.
@@ -223,7 +223,7 @@ Ltac simpl_PCond FLD :=
Ltac simpl_PCond_BEURK FLD :=
let req := get_FldEq FLD in
let lemma := get_CondLemma FLD in
- (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
+ (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
protect_fv "field_cond";
fold_field_cond req.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 07:24:18 +0000