Added initial support for inversion principles in Matita NG.

[helm.git] / helm / software / components / ng_kernel / nCic.ml

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index f39cf868e32fe905a123e4c8b3f516d67e4a68f7..fead92210f45053b925c7acbc82aeb6f55b64cce 100644 (file)
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -22,7 +22,8 @@ type universe = (univ_algebra * NUri.uri) list
 type sort = Prop | Type of universe
 
 type implicit_annotation =
- [ `Closed | `Type | `Hole | `Term | `Typeof of int | `Vector ]
+ [ `Closed | `Type | `Hole | `Tagged of string | `Term | `Typeof of int | `Vector ]
+
 
 type lc_kind = Irl of int | Ctx of term list