diff options
| author | herbelin | 2001-01-31 11:25:37 +0000 |
|---|---|---|
| committer | herbelin | 2001-01-31 11:25:37 +0000 |
| commit | 847d01260e3a42853421e0ddb5c34a0058d1f5a9 (patch) | |
| tree | 958583839c0189e472d0d27cdc5f7b02530bea0f | |
| parent | 7de3189d5f82e11a8f584dd1a6104c7863dcc2b4 (diff) | |
Ajout option Set/Unset/Test Printing Coercions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1298 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_basevernac.ml4 | 8 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 23 |
2 files changed, 31 insertions, 0 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 4e4be99d5f..def0127333 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -173,6 +173,14 @@ GEXTEND Gram | IDENT "Test"; IDENT "Implicit"; IDENT "Arguments" -> <:ast< (TEST_IMPLICIT_ARGS) >> + (* Set printing of coercions *) + | "Set"; IDENT "Printing"; IDENT "Coercions" -> + <:ast< (PRINTING_COERCIONS_ON) >> + | IDENT "Unset"; IDENT "Printing"; IDENT "Coercions" -> + <:ast< (PRINTING_COERCIONS_OFF) >> + | IDENT "Test"; IDENT "Printing"; IDENT "Coercions" -> + <:ast< (TEST_PRINTING_COERCIONS) >> + (* Pour intervenir sur les tables de paramètres *) | "Set"; table = identarg; field = identarg; value = option_value -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 67e06e9501..96fbd375d8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -472,6 +472,29 @@ let _ = message "Implicit arguments mode is unset") | _ -> bad_vernac_args "IMPLICIT_ARGS_OFF") +let _ = + add "PRINTING_COERCIONS_ON" + (function + | [] -> (fun () -> Termast.print_coercions := true) + | _ -> bad_vernac_args "PRINTING_COERCIONS_ON") + +let _ = + add "PRINTING_COERCIONS_OFF" + (function + | [] -> (fun () -> Termast.print_coercions := false) + | _ -> bad_vernac_args "PRINTING_COERCIONS_OFF") + +let _ = + add "TEST_PRINTING_COERCIONS" + (function + | [] -> + (fun () -> + if !(Termast.print_coercions) = true then + message "Printing of coercions is set" + else + message "Printing of coercions is unset") + | _ -> bad_vernac_args "TEST_PRINTING_COERCIONS") + let number_list = List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list") |