Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_basevernac.ml4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1332 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 56 insertions, 8 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 96fbd375d..d8389ac05 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -472,29 +472,77 @@ let _ =
 		message "Implicit arguments mode is unset")
        | _  -> bad_vernac_args "IMPLICIT_ARGS_OFF")
 
-let _ =          
+let coercion_of_qualid loc qid =
+  let ref = global loc qid in
+  let coe = Classops.coe_of_reference ref in
+  if not (Classops.coercion_exists coe) then
+    errorlabstrm "try_add_coercion" 
+      [< Printer.pr_global ref; 'sTR" is not a coercion" >];
+  coe
+
+let _ =
   add "PRINTING_COERCIONS_ON"
     (function 
        | [] -> (fun () -> Termast.print_coercions := true)
-       | _  -> bad_vernac_args "PRINTING_COERCIONS_ON")
+       | l ->
+	   let ql =
+	     List.map 
+	       (function
+		  | VARG_QUALID qid -> qid
+		  | _ ->  bad_vernac_args "PRINTING_COERCIONS_ON") l in
+	   (fun () ->
+	      List.iter
+		(fun qid ->
+		   Classops.set_coercion_visibility true
+		     (coercion_of_qualid dummy_loc qid))
+		ql))
 
 let _ =
   add "PRINTING_COERCIONS_OFF"
     (function 
        | [] -> (fun () -> Termast.print_coercions := false)
-       | _  -> bad_vernac_args "PRINTING_COERCIONS_OFF")
+       | l -> 
+	   let ql =
+	     List.map 
+	       (function
+		  | VARG_QUALID qid -> qid
+		  | _ ->  bad_vernac_args "PRINTING_COERCIONS_OFF") l in
+	   (fun () ->
+	      List.iter
+		(fun qid ->
+		   Classops.set_coercion_visibility false 
+		     (coercion_of_qualid dummy_loc qid))
+		ql))
 
 let _ =
   add "TEST_PRINTING_COERCIONS"
     (function 
        | [] ->
-	   (fun () ->
-	      if !(Termast.print_coercions) = true then
+           (fun () ->
+              if !(Termast.print_coercions) = true then
 		message "Printing of coercions is set"
-	      else 
+              else 
 		message "Printing of coercions is unset")
-       | _  -> bad_vernac_args "TEST_PRINTING_COERCIONS")
-
+       | l -> 
+	   let ql =
+	     List.map 
+	       (function
+		  | VARG_QUALID qid -> qid
+		  | _  -> bad_vernac_args "TEST_PRINTING_COERCIONS") l in
+	   (fun () ->
+              List.iter
+		(fun qid ->
+		   let coe = coercion_of_qualid dummy_loc qid in
+	           if Classops.is_coercion_visible coe then
+		     message
+		       ("Printing of coercion "^(string_of_qualid qid)^
+			" is set")
+		   else 
+		     message 
+		       ("Printing of coercion "^(string_of_qualid qid)^
+			" is unset"))
+		ql))
+    
 let number_list = 
   List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list")