cicDischarge: new module for discharging the explicit variables occurring in a

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

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index df436e7097cefe67fb842f59414a9f3258ad6b12..189d172f88e2ed327c516c96710d6da68ec29ba6 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -260,14 +260,14 @@ let pp_macro ~term_pp =
   in
   let flavour_pp = function
      | None                   -> ""
-     | Some `Definition       -> "as definition"
-     | Some `MutualDefinition -> "as mutual"
-     | Some `Fact             -> "as fact"
-     | Some `Lemma            -> "as lemma"
-     | Some `Remark           -> "as remark"
-     | Some `Theorem          -> "as theorem"
-     | Some `Variant          -> "as variant"
-     | Some `Axiom            -> "as axiom"
+     | Some `Definition       -> " as definition"
+     | Some `MutualDefinition -> " as mutual"
+     | Some `Fact             -> " as fact"
+     | Some `Lemma            -> " as lemma"
+     | Some `Remark           -> " as remark"
+     | Some `Theorem          -> " as theorem"
+     | Some `Variant          -> " as variant"
+     | Some `Axiom            -> " as axiom"
   in
   function 
   (* Whelp *)