Let's use already existent functions.

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 81b577093ab3e1f2dca23afb84c22883e56ee1e7..6deaaf572b7914f9ad3edba29b1a937b4bc1a711 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -466,7 +466,7 @@ let mk_meta ?(attrs=[]) metasenv context ?with_type kind =
   let n = newmeta () in
   let ty= match with_type with None-> NCic.Implicit (`Typeof n)| Some x ->x in
   let len = List.length context in
-  let attrs = (kind :> NCic.meta_attr) :: attrs in
+  let attrs = NCicUntrusted.set_kind kind attrs in
   let menv_entry = (n, (attrs, context, ty)) in
   menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
 ;;