diff options
Diffstat (limited to 'common/Smallstep.v')
| -rw-r--r-- | common/Smallstep.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/common/Smallstep.v b/common/Smallstep.v index 487e7a80..3cbd8934 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -552,6 +552,8 @@ Definition Semantics {state funtype vartype: Type} (** Handy notations. *) +Declare Scope smallstep_scope. + Notation " 'Step' L " := (step L (globalenv L)) (at level 1) : smallstep_scope. Notation " 'Star' L " := (star (step L) (globalenv L)) (at level 1) : smallstep_scope. Notation " 'Plus' L " := (plus (step L) (globalenv L)) (at level 1) : smallstep_scope. |