helm/software/components/ng_refiner/oMeta2nMeta.ml

   1 let convert_metasenv uri =
   2   let new_metasenv, fixpoints =
   3     List.fold_left
   4       (fun (nm,fty) (i, ctx, ty) ->
   5          let new_ty, fix_ty = OCic2NCic.convert_term uri ty in
   6
   7   in
   8   assert (fixpoints = []);
   9   new_metasenv
  10 ;;