diff options
| author | Hugo Herbelin | 2018-03-30 14:47:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 13:07:29 +0200 |
| commit | 46ab3659dd1f2e4839064cfabc03bd19268fa44b (patch) | |
| tree | a4b215eb3289a189c9756bf44c3e52d04f306c99 /plugins/ssr | |
| parent | 8e675d70ad1f60cbbf9f1e630ce6dee61347c7ca (diff) | |
Adapting standard library to the introduction of "Declare Scope".
Removing in passing two Local which are no-ops in practice.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssreflect.v | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrfun.v | 2 |
2 files changed, 5 insertions, 0 deletions
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index b4144aa45e..460bdc6d23 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -86,6 +86,7 @@ Export SsrSyntax. (* recognize the expansion of the boolean if; using the default printer *) (* avoids a spurrious trailing %GEN_IF. *) +Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. Notation "'if' c 'then' v1 'else' v2" := @@ -103,6 +104,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := (* Force boolean interpretation of simple if expressions. *) +Declare Scope boolean_if_scope. Delimit Scope boolean_if_scope with BOOL_IF. Notation "'if' c 'return' t 'then' v1 'else' v2" := @@ -125,6 +127,7 @@ Open Scope boolean_if_scope. (* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *) (* Lists library) should be loaded before ssreflect so that their notations *) (* do not mask all ssreflect forms. *) +Declare Scope form_scope. Delimit Scope form_scope with FORM. Open Scope form_scope. diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index b2d5143e36..99ff943e61 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -216,6 +216,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope fun_scope. Delimit Scope fun_scope with FUN. Open Scope fun_scope. @@ -225,6 +226,7 @@ Notation "f ^~ y" := (fun x => f x y) Notation "@^~ x" := (fun f => f x) (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope. +Declare Scope pair_scope. Delimit Scope pair_scope with PAIR. Open Scope pair_scope. |