diff options
Diffstat (limited to 'mathcomp/ssreflect/plugin/v8.4')
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 index 49a5912..1c22477 100644 --- a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 @@ -9,10 +9,7 @@ let () = Mltop.add_known_plugin (fun () -> Printf.printf "\nSmall Scale Reflection version %s loaded.\n" ssrversion; Printf.printf "Copyright 2005-2012 Microsoft Corporation and INRIA.\n"; Printf.printf "Distributed under the terms of the CeCILL-B license.\n\n" - end; - (* Disable any semantics associated with bullets *) - Goptions.set_string_option_value_gen - (Some false) ["Bullet";"Behavior"] "None") + end) "ssreflect" ;; (* Defining grammar rules with "xx" in it automatically declares keywords too *) |