aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bb66658a37..fe50bd4b08 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -107,7 +107,7 @@ let _show_inactive_notations () =
let deactivate_notation nr =
match nr with
| SynDefRule kn ->
- (* shouldn't we check wether it is well defined? *)
+ (* shouldn't we check whether it is well defined? *)
inactive_notations_table := IRuleSet.add nr !inactive_notations_table
| NotationRule (scopt, ntn) ->
match availability_of_notation (scopt, ntn) (scopt, []) with