X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=f12b50d5ddc62c651ff8cca045320169776cc7b3;hb=dd627e471392375ca7b6dad78a931a8682e06dbe;hp=2fa02c30747ee67008c474b85d29187a365a8925;hpb=433e66b381d1b89e48c05d517494fc300fd0abb5;p=helm.git

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index 2fa02c307..f12b50d5d 100644
--- a/matita/components/ng_tactics/nTacStatus.ml
+++ b/matita/components/ng_tactics/nTacStatus.ml
@@ -232,6 +232,15 @@ let normalize status ?delta ctx t =
   status, (ctx, t)
 ;;
   
+let are_convertible status ctx a b =
+  let status, (_,a) = relocate status ctx a in
+  let status, (_,b) = relocate status ctx b in
+  let n,h,metasenv,subst,o = status#obj in
+  let res = NCicReduction.are_convertible status metasenv subst ctx a b in
+   status, res
+;;
+let are_convertible a b c d = wrap "are_convertible" (are_convertible a b c) d;;
+
 let unify status ctx a b =
   let status, (_,a) = relocate status ctx a in
   let status, (_,b) = relocate status ctx b in