]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAst.ml
fix for instance
[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml
index 23a8b8e6755c34071a78bdd1419a9ea5e6118808..e01b7e7edf2985559668d517fedd7be60781b08b 100644 (file)
@@ -97,6 +97,7 @@ type 'term macro =
   | Check of loc * 'term 
   | Hint of loc
   | Match of loc * 'term 
+  | Instance of loc * 'term 
   | Quit of loc
   | Redo of loc * int option
   | Undo of loc * int option