aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Wellfounded/Lexicographic_Exponentiation.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Wellfounded/Lexicographic_Exponentiation.v')
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v14
1 files changed, 7 insertions, 7 deletions
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: