From 106db6ec639e23ab8af56a1d889b3670fa292d6f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 Oct 2009 15:53:17 +0000 Subject: [PATCH] Let's use already existent functions. --- helm/software/components/ng_refiner/nCicMetaSubst.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 81b577093..6deaaf572 100644 --- 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 ;; -- 2.39.2