]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/cicTextualParser2.ml
added instance
[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml
index 34b3d01e0cc18a72dde5f36c0953930b46989681..e7506a15d7b140adcef126ce8a78d87a5cfd48f2 100644 (file)
@@ -482,6 +482,7 @@ EXTEND
         TacticAst.Check (loc, t)
     | [ IDENT "hint" ] -> TacticAst.Hint loc
     | [ IDENT "pmatch" ] ; t = term -> TacticAst.Match (loc,t)
+    | [ IDENT "instance" ] ; t = term -> TacticAst.Instance (loc,t)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
   ]];