Using Prop conjuction on Props lowers the universes.

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 721cb0eff1a2c0a8de19cd3c6873bfb7a0005961..26dd9b9e050ddb2707997ee69ea7cfb43978d3f0 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -169,6 +169,8 @@ EXTEND
         GrafiteAst.Absurd (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
+    | IDENT "applyP"; t = tactic_term ->
+        GrafiteAst.ApplyP (loc, t)
     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
         GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->