- refine's type_of no longer return a substitution

[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index a28b853bebabcfe3eb9be907cedd24bda2bff868..ba8ae7d98cd04606ee60fa7cf779f333482e0eca 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -475,6 +475,14 @@ let rec apply_subst_context subst context =
       | None -> None :: context)
     context []
 
+let apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, apply_subst_context subst context, apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+      metasenv)
+
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
 let ppcontext ?(sep = "\n") subst context =