]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_refiner/oMeta2nMeta.ml
4993e482a515c9e41626e6cc78ae6c48b437b4cf
[helm.git] / matita / 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 ;;