X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=03de06d1c6c3306613b31e77b2f24639be93ec3f;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=6664a5b9781cf0b06bb465c78f9f017558d6c522;hpb=7ca0a000878e864c92d94f77900bc2ca0ac143b9;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 6664a5b97..03de06d1c 100644
--- 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")))