X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=118261af027c2efa101facb0d21a39d611b03a0e;hp=fc525c84a772034db42886a5359e540da26de1f7;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hpb=f00a612006ac05f49a42ab507a95d3298bc1457a

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index fc525c84a..118261af0 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
@@ -460,7 +469,7 @@ let analyse_indty status ty =
  let _,_,_,cl = List.nth tl i in
  let consno = List.length cl in
  let left, right = HExtlib.split_nth lno args in
- status, (ref, consno, left, right)
+ status, (ref, consno, left, right, cl)
 ;;
 
 let apply_subst status ctx t =