- | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
- | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
- | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+ | `Closed ->
+ let metasenv,subst,expty =
+ match expty with
+ None -> metasenv,subst,None
+ | Some typ ->
+ let (metasenv,subst),typ =
+ try
+ NCicMetaSubst.delift
+ ~unify:(fun m s c t1 t2 ->
+ try Some (NCicUnification.unify rdb m s c t1 t2)
+ with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
+ metasenv subst context 0 (0,NCic.Irl 0) typ
+ with
+ NCicMetaSubst.MetaSubstFailure _
+ | NCicMetaSubst.Uncertain _ ->
+ raise (RefineFailure (lazy (localise t,"Trying to create a closed meta with a non closed type")))
+
+ in
+ metasenv,subst,Some typ
+ in
+ NCicMetaSubst.mk_meta metasenv [] (foo `Term expty),subst
+ | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type expty),subst
+ | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term expty),subst