diff options
Diffstat (limited to 'contrib/romega/ReflOmegaCore.v')
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 46512aab0..31ca8f804 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -879,7 +879,7 @@ Infix "+" := Tplus : romega_scope. Infix "*" := Tmult : romega_scope. Infix "-" := Tminus : romega_scope. Notation "- x" := (Topp x) : romega_scope. -Notation "[ x ]" := (Tvar x) (at level 1) : romega_scope. +Notation "[ x ]" := (Tvar x) : romega_scope. (* \subsubsection{Definition of reified goals} *) |