- library/list/list.ma: unused code commented

[helm.git] / helm / software / components / grafite / grafiteAst.ml

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 6b9a3eba18a632837b1ad66221169a6b34979c83..e86cb082f7e1440d8712ec4cbc8ff052ed0d04bb 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -150,13 +150,14 @@ type print_kind = [ `Env | `Coer ]
 
 type inline_param = IPPrefix of string         (* undocumented *)
                  | IPAs of Cic.object_flavour (* preferred flavour *)
+                 | IPCoercions                (* show coercions *)
+                  | IPDebug of int             (* set debug level *)
                   | IPProcedural               (* procedural rendering *)
                   | IPNoDefaults               (* no default-based tactics *)
                  | IPLevel of int             (* granularity level *)
                   | IPDepth of int             (* undocumented *)
                   | IPComments                 (* show statistics *)
-                 | IPCoercions                (* show coercions *)
-                  | IPDebug of int             (* set debug level *)
+                  | IPCR                       (* detect convertible rewriting *)
 
 type ('term,'lazy_term) macro = 
   (* Whelp's stuff *)