X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=f8a73f2f53b0fd4e00cfb3e73f4d832def6a2fd3;hb=6d9de12a536ee4b9e369849ff7e9aa4ca464de9d;hp=04cf03c67b81f4b70eafd229694b71ffec9b162d;hpb=cc3d3e3f697e06026680bc94988c782ddd8eb33e;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 04cf03c67..f8a73f2f5 100644
--- 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