ported to latest lablgtk2 snapshot

[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 04cf03c67b81f4b70eafd229694b71ffec9b162d..f8a73f2f53b0fd4e00cfb3e73f4d832def6a2fd3 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -483,6 +483,11 @@ let whd subst context term =
     raise (MetaSubstFailure ("Weak head reduction failure: " ^
       Printexc.to_string e))
 
+let are_convertible subst context t1 t2 =
+  let context = apply_subst_context subst context in
+  let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in
+  CicReduction.are_convertible context t1 t2
+
 let type_of_aux' metasenv subst context term =
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in