diff options
author | 2003-10-16 14:52:09 +0000 | |
---|---|---|
committer | 2003-10-16 14:52:09 +0000 | |
commit | 4d61b0c12eb94e220740e39e10a7678cdc0a5a85 (patch) | |
tree | 6f070cffd72473b1c22301929b617d90eb6ce842 /toplevel/vernacentries.ml | |
parent | 214759f4b785489932031d0651a7c8a85f49ab1d (diff) |
Debranchement de l'affichage systematique des projections avec la notation pointee; soumis maintenant a l'activation de l'option 'Set Printing Projections'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4649 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b9150a30e..3f979d9b1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -722,6 +722,14 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "projection printing using dot notation"; + optkey = (SecondaryTable ("Printing","Projections")); + optread = (fun () -> !Constrextern.print_projections); + optwrite = (fun b -> Constrextern.print_projections := b) } + +let _ = + declare_bool_option + { optsync = true; optname = "symbols printing"; optkey = (SecondaryTable ("Printing",if !Options.v7 then "Symbols" else "Notations")); optread = (fun () -> not !Constrextern.print_no_symbol); |