Added initial support for inversion principles in Matita NG.

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 6664a5b9781cf0b06bb465c78f9f017558d6c522..03de06d1c6c3306613b31e77b2f24639be93ec3f 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -42,6 +42,7 @@ let exp_implicit ~localise metasenv context expty t =
   | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
   | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
   | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+  | `Tagged s -> NCicMetaSubst.mk_meta ~name:s metasenv context (foo `Term)
   | `Vector ->
       raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
        "can only be used in argument position")))