aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.ml27
-rw-r--r--theories/Classes/RelationClasses.v26
-rw-r--r--theories/Init/Datatypes.v29
-rw-r--r--theories/Lists/List.v66
-rw-r--r--theories/Relations/Relation_Operators.v2
5 files changed, 79 insertions, 71 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 6ae720fca..39ae27823 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -147,18 +147,23 @@ let delimiters_map = ref Gmap.empty
let declare_delimiters scope key =
let sc = find_scope scope in
- if sc.delimiters <> None && Flags.is_verbose () then begin
- let old = Option.get sc.delimiters in
- Flags.if_verbose
- warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
+ let newsc = { sc with delimiters = Some key } in
+ begin match sc.delimiters with
+ | None -> scope_map := Gmap.add scope newsc !scope_map
+ | Some oldkey when oldkey = key -> ()
+ | Some oldkey ->
+ Flags.if_verbose warning
+ ("Overwritting previous delimiting key "^oldkey^" in scope "^scope);
+ scope_map := Gmap.add scope newsc !scope_map
end;
- let sc = { sc with delimiters = Some key } in
- scope_map := Gmap.add scope sc !scope_map;
- if Gmap.mem key !delimiters_map then begin
- let oldsc = Gmap.find key !delimiters_map in
- Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
- end;
- delimiters_map := Gmap.add key scope !delimiters_map
+ try
+ let oldscope = Gmap.find key !delimiters_map in
+ if oldscope = scope then ()
+ else begin
+ Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldscope);
+ delimiters_map := Gmap.add key scope !delimiters_map
+ end
+ with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map
let find_delimiters_scope loc key =
try Gmap.find key !delimiters_map
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index cc3cae4da..06da51129 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -203,13 +203,11 @@ Program Instance iff_equivalence : Equivalence iff.
The resulting theory can be applied to homogeneous binary relations but also to
arbitrary n-ary predicates. *)
-Require Import Coq.Lists.List.
+Local Open Scope list_scope.
(* Notation " [ ] " := nil : list_scope. *)
(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
-(* Open Local Scope list_scope. *)
-
(** A compact representation of non-dependent arities, with the codomain singled-out. *)
Fixpoint arrows (l : list Type) (r : Type) : Type :=
@@ -220,9 +218,9 @@ Fixpoint arrows (l : list Type) (r : Type) : Type :=
(** We can define abbreviations for operation and relation types based on [arrows]. *)
-Definition unary_operation A := arrows (cons A nil) A.
-Definition binary_operation A := arrows (cons A (cons A nil)) A.
-Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A.
+Definition unary_operation A := arrows (A::nil) A.
+Definition binary_operation A := arrows (A::A::nil) A.
+Definition ternary_operation A := arrows (A::A::A::nil) A.
(** We define n-ary [predicate]s as functions into [Prop]. *)
@@ -230,11 +228,11 @@ Notation predicate l := (arrows l Prop).
(** Unary predicates, or sets. *)
-Definition unary_predicate A := predicate (cons A nil).
+Definition unary_predicate A := predicate (A::nil).
(** Homogeneous binary relations, equivalent to [relation A]. *)
-Definition binary_relation A := predicate (cons A (cons A nil)).
+Definition binary_relation A := predicate (A::A::nil).
(** We can close a predicate by universal or existential quantification. *)
@@ -345,18 +343,18 @@ Program Instance predicate_implication_preorder :
from the general ones. *)
Definition relation_equivalence {A : Type} : relation (relation A) :=
- @predicate_equivalence (cons _ (cons _ nil)).
+ @predicate_equivalence (_::_::nil).
Class subrelation {A:Type} (R R' : relation A) : Prop :=
- is_subrelation : @predicate_implication (cons A (cons A nil)) R R'.
+ is_subrelation : @predicate_implication (A::A::nil) R R'.
Implicit Arguments subrelation [[A]].
Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
- @predicate_intersection (cons A (cons A nil)) R R'.
+ @predicate_intersection (A::A::nil) R R'.
Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
- @predicate_union (cons A (cons A nil)) R R'.
+ @predicate_union (A::A::nil) R R'.
(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
@@ -364,10 +362,10 @@ Set Automatic Introduction.
Instance relation_equivalence_equivalence (A : Type) :
Equivalence (@relation_equivalence A).
-Proof. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
+Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed.
Instance relation_implication_preorder A : PreOrder (@subrelation A).
-Proof. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
+Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed.
(** *** Partial Order.
A partial order is a preorder which is additionally antisymmetric.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 8d790d1fd..75bf27702 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -226,6 +226,35 @@ Qed.
Definition ID := forall A:Type, A -> A.
Definition id : ID := fun A x => x.
+(** Polymorphic lists and some operations *)
+
+Inductive list (A : Type) : Type :=
+ | nil : list A
+ | cons : A -> list A -> list A.
+
+Implicit Arguments nil [A].
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+Delimit Scope list_scope with list.
+Bind Scope list_scope with list.
+
+Local Open Scope list_scope.
+
+Fixpoint length (A : Type) (l:list A) : nat :=
+ match l with
+ | nil => O
+ | _ :: l' => S (length l')
+ end.
+
+(** Concatenation of two lists *)
+
+Fixpoint app (A : Type) (l m:list A) : list A :=
+ match l with
+ | nil => m
+ | a :: l1 => a :: app l1 m
+ end.
+
+Infix "++" := app (right associativity, at level 60) : list_scope.
+
(* begin hide *)
(* Compatibility *)
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 37802d4bc..01b1c066a 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -17,79 +17,43 @@ Set Implicit Arguments.
(** * Basics: definition of polymorphic lists and some operations *)
(******************************************************************)
-(** ** Definitions *)
+(** The definition of [list] is now in [Init/Datatypes],
+ as well as the definitions of [length] and [app] *)
+
+Open Scope list_scope.
Section Lists.
Variable A : Type.
- Inductive list : Type :=
- | nil : list
- | cons : A -> list -> list.
-
- Infix "::" := cons (at level 60, right associativity) : list_scope.
-
- Open Scope list_scope.
-
(** Head and tail *)
- Definition head (l:list) :=
+ Definition head (l:list A) :=
match l with
| nil => error
| x :: _ => value x
end.
- Definition hd (default:A) (l:list) :=
+ Definition hd (default:A) (l:list A) :=
match l with
| nil => default
| x :: _ => x
end.
- Definition tail (l:list) : list :=
+ Definition tail (l:list A) : list A :=
match l with
| nil => nil
| a :: m => m
end.
- (** Length of lists *)
- Fixpoint length (l:list) : nat :=
- match l with
- | nil => 0
- | _ :: m => S (length m)
- end.
-
(** The [In] predicate *)
- Fixpoint In (a:A) (l:list) {struct l} : Prop :=
+ Fixpoint In (a:A) (l:list A) : Prop :=
match l with
| nil => False
| b :: m => b = a \/ In a m
end.
-
- (** Concatenation of two lists *)
- Fixpoint app (l m:list) {struct l} : list :=
- match l with
- | nil => m
- | a :: l1 => a :: app l1 m
- end.
-
- Infix "++" := app (right associativity, at level 60) : list_scope.
-
End Lists.
-(** Exporting list notations and tactics *)
-
-Implicit Arguments nil [A].
-Infix "::" := cons (at level 60, right associativity) : list_scope.
-Infix "++" := app (right associativity, at level 60) : list_scope.
-
-Open Scope list_scope.
-
-Delimit Scope list_scope with list.
-
-Bind Scope list_scope with list.
-
-Arguments Scope list [type_scope].
-
(** ** Facts about lists *)
Section Facts.
@@ -1950,7 +1914,19 @@ Ltac simpl_list := autorewrite with list.
Ltac ssimpl_list := autorewrite with list using simpl.
(* begin hide *)
-(* Compatibility *)
+(* Compatibility notations after the migration of [list] to [Datatypes] *)
+Notation list := list (only parsing).
+Notation list_rect := list_rect (only parsing).
+Notation list_rec := list_rec (only parsing).
+Notation list_ind := list_ind (only parsing).
+Notation nil := @nil (only parsing).
+Notation cons := @cons (only parsing).
+Notation length := @length (only parsing).
+Notation app := @app (only parsing).
+(* We hide these compatibility notations behind the true definitions
+ that are in [Datatypes]: *)
+Export Datatypes.
+(* Compatibility Names *)
Notation ass_app := app_assoc (only parsing).
Notation app_ass := app_assoc_reverse (only parsing).
Hint Resolve app_nil_end : datatypes v62.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 8fea0abc4..39e0331d5 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -17,7 +17,6 @@
(************************************************************************)
Require Import Relation_Definitions.
-Require Import List.
(** * Some operators to build relations *)
@@ -187,6 +186,7 @@ Section Swap.
| sp_swap x y (p:A * A) : symprod A A R R (x, y) p -> swapprod (y, x) p.
End Swap.
+Local Open Scope list_scope.
Section Lexicographic_Exponentiation.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-15 00:20:16 +0000