diff options
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 6 | ||||
| -rw-r--r-- | test-suite/modules/sub_objects.v | 2 | ||||
| -rw-r--r-- | test-suite/success/CasesDep.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 14 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 7 | ||||
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Union.v | 2 |
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. |