X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=813a080719cfbf039ea234c4dab8e1c81460004a;hb=948bb5d710c5d7f3185b6fef76c8e71f247cc664;hp=60e3aac4bfa0d2ad8ba476ecf1082c434cf22f1c;hpb=4442acec319822fbc4eb2e873808dbfc1893f390;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 60e3aac4b..813a08071 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -214,6 +214,7 @@ type ncommand =
   | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
   | NObj of loc * CicNotationPt.term CicNotationPt.obj
   | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
+  | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string *
       CicNotationPt.term * CicNotationPt.term *
       (string * CicNotationPt.term) * CicNotationPt.term