Commit 42f415cc authored by MARCHE Claude's avatar MARCHE Claude

doc: replace obsolete occurrences of `namespace` by `scope`

Note that the text itself uses much more the term "namespace" than scope,
it would be better to update it accordingly
parent 4b4835d6
......@@ -8,7 +8,7 @@
| "let" "rec" rec-defn ;
| "val" "ghost"? lident-nq label* pgm-decl ;
| "exception" lident-nq label* type? ;
| "namespace" "import"? uident-nq mdecl* "end" ;
| "scope" "import"? uident-nq mdecl* "end" ;
\
mtype-decl ::= lident-nq label* ("'" lident-nq label*)* ;
mtype-defn ;
......
......@@ -305,7 +305,7 @@ would be \texttt{T.$s$}.
the instruction ``\texttt{clone import Order as O}'' can be equivalently
written as:
\begin{whycode}
namespace import O
scope import O
clone export Order
end
\end{whycode}
......
......@@ -12,7 +12,8 @@
| "goal" ident-nq ":" formula ;
| "use" imp-exp tqualid ("as" uident)? ;
| "clone" imp-exp tqualid ("as" uident)? subst? ;
| "namespace" "import"? uident-nq decl* "end" ;
| "scope" "import"? uident-nq decl* "end" ;
| "import" uident ;
\
logic-decl ::= function-decl ;
| predicate-decl
......@@ -38,7 +39,7 @@
subst-elt ::= "type" lqualid "=" lqualid ;
| "function" lqualid "=" lqualid ;
| "predicate" lqualid "=" lqualid ;
| "namespace" (uqualid | ".") "=" (uqualid | ".") ;
| "scope" (uqualid | ".") "=" (uqualid | ".") ;
| "lemma" qualid ;
| "goal" qualid ;
\
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment