diff options
| author | Robbert Krebbers | 2016-01-12 22:07:00 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2016-01-12 22:07:00 +0100 |
| commit | ad273277ab38bfe458e9332dea5f3a79e3885567 (patch) | |
| tree | 869c83ca95fd6dc9579e7ec12fd89f1ba1c9dbea | |
| parent | be7249377b78f44465746be61b1f40830aa213e5 (diff) | |
Move bullet initialization to ssreflect.v
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 1 |
4 files changed, 4 insertions, 12 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 6e805a9..8bedfb0 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -10,10 +10,7 @@ let () = Mltop.add_known_plugin (fun () -> Printf.printf "\nSmall Scale Reflection version %s loaded.\n" ssrversion; Printf.printf "Copyright 2005-2014 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" ;; 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 *) diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 index 72f1949..06c6a6c 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 @@ -10,10 +10,7 @@ let () = Mltop.add_known_plugin (fun () -> Printf.printf "\nSmall Scale Reflection version %s loaded.\n" ssrversion; Printf.printf "Copyright 2005-2014 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" ;; diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 4a3cfc7..1ff82ab 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -51,6 +51,7 @@ Global Set Asymmetric Patterns. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Global Set Bullet Behavior "None". Module SsrSyntax. |