aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--contrib/romega/ReflOmegaCore.v6
-rw-r--r--test-suite/modules/sub_objects.v2
-rw-r--r--test-suite/success/CasesDep.v2
-rw-r--r--theories/Wellfounded/Disjoint_Union.v2
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v14
-rw-r--r--theories/Wellfounded/Lexicographic_Product.v7
-rw-r--r--theories/Wellfounded/Transitive_Closure.v2
-rw-r--r--theories/Wellfounded/Union.v2
8 files changed, 18 insertions, 19 deletions
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 0df34f422..f4eea6c2f 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -50,7 +50,7 @@ Inductive proposition : Set :=
| NeqTerm: term -> term -> proposition.
(* Définition des hypothèses *)
-Syntactic Definition hyps := (list proposition).
+Notation hyps := (list proposition).
Definition absurd := (cons FalseTerm (nil proposition)).
@@ -413,7 +413,7 @@ Save.
(* \subsubsection{Généralisation à des listes de buts (disjonctions)} *)
-Syntactic Definition lhyps := (list hyps).
+Notation lhyps := (list hyps).
Fixpoint interp_list_hyps [env: (list Z); l : lhyps] : Prop :=
Cases l of
@@ -1778,7 +1778,7 @@ Inductive t_omega : Set :=
| O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega
| O_STATE : Z -> step -> nat -> nat -> t_omega -> t_omega.
-Syntactic Definition singleton := [a: hyps] (cons a (nil hyps)).
+Notation singleton := [a: hyps] (cons a (nil hyps)).
Fixpoint execute_omega [t: t_omega] : hyps -> lhyps :=
[l : hyps] Cases t of
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
index 73fd6f322..2dbac3407 100644
--- a/test-suite/modules/sub_objects.v
+++ b/test-suite/modules/sub_objects.v
@@ -14,7 +14,7 @@ Module M.
Definition idid:=[A:Set][x:A](id x).
Grammar constr constr8 :=
not_eq [ "#" constr7($b) ] -> [ (idid $b) ].
- Syntactic Definition inc := (plus (S O)).
+ Notation inc := (plus (S O)).
End N.
Definition zero:=(N.idid O).
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 5dd687859..8d0dc0f5c 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -109,7 +109,7 @@ Definition Map_setoid := (Build_Setoid Map ext Equiv_map_eq).
End Maps.
-Syntactic Definition ap := (explicit_ap ? ?).
+Notation ap := (explicit_ap ? ?).
Grammar constr constr8 :=
map_setoid [ constr7($c1) "=>" constr8($c2) ]
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index ac3233704..6e9cbf062 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -19,7 +19,7 @@ Variable A,B:Set.
Variable leA: A->A->Prop.
Variable leB: B->B->Prop.
-Syntactic Definition Le_AsB := (le_AsB A B leA leB).
+Notation Le_AsB := (le_AsB A B leA leB).
Lemma acc_A_sum: (x:A)(Acc A leA x)->(Acc A+B Le_AsB (inl A B x)).
Proof.
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index ad157ea9d..5c73cdae0 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -23,15 +23,15 @@ Section Wf_Lexicographic_Exponentiation.
Variable A:Set.
Variable leA: A->A->Prop.
-Syntactic Definition Power := (Pow A leA).
-Syntactic Definition Lex_Exp := (lex_exp A leA).
-Syntactic Definition ltl := (Ltl A leA).
-Syntactic Definition Descl := (Desc A leA).
+Notation Power := (Pow A leA).
+Notation Lex_Exp := (lex_exp A leA).
+Notation ltl := (Ltl A leA).
+Notation Descl := (Desc A leA).
-Syntactic Definition List := (list A).
-Syntactic Definition Nil := (nil A).
+Notation List := (list A).
+Notation Nil := (nil A).
(* useless but symmetric *)
-Syntactic Definition Cons := (cons 1!A).
+Notation Cons := (cons 1!A).
Syntax constr
level 1:
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 3e8ba318a..39b00e676 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -23,8 +23,7 @@ Variable B:A->Set.
Variable leA: A->A->Prop.
Variable leB: (x:A)(B x)->(B x)->Prop.
-
-Syntactic Definition LexProd := (lexprod A B leA leB).
+Notation LexProd := (lexprod A B leA leB).
Hints Resolve t_step Acc_clos_trans wf_clos_trans.
@@ -86,7 +85,7 @@ Section Wf_Symmetric_Product.
Variable leA: A->A->Prop.
Variable leB: B->B->Prop.
- Syntactic Definition Symprod := (symprod A B leA leB).
+ Notation Symprod := (symprod A B leA leB).
(*i
Local sig_prod:=
@@ -135,7 +134,7 @@ Section Swap.
Variable A:Set.
Variable R:A->A->Prop.
- Syntactic Definition SwapProd :=(swapprod A R).
+ Notation SwapProd :=(swapprod A R).
Lemma swap_Acc: (x,y:A)(Acc A*A SwapProd (x,y))->(Acc A*A SwapProd (y,x)).
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 1cb9848f6..1198c1d47 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -17,7 +17,7 @@ Section Wf_Transitive_Closure.
Variable A: Set.
Variable R: (relation A).
- Syntactic Definition trans_clos := (clos_trans A R).
+ Notation trans_clos := (clos_trans A R).
Lemma incl_clos_trans: (inclusion A R trans_clos).
Red;Auto with sets.
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 9c013bd11..084538d8c 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -18,7 +18,7 @@ Section WfUnion.
Variable A: Set.
Variable R1,R2: (relation A).
- Syntactic Definition Union := (union A R1 R2).
+ Notation Union := (union A R1 R2).
Hints Resolve Acc_clos_trans wf_clos_trans.