X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=b13de05d6d0c9ba1fb2d902ea52a74d35f5fb9af;hb=b804ff9f8fba300ffaa54add291e0f6490b757ce;hp=577edf9d903a889fd536aca8e127bbee60f717f4;hpb=751af6075f28fb2abe052de73630ce114e761dee;p=helm.git

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 577edf9d9..b13de05d6 100644
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -261,10 +261,13 @@ let repeat_tac t s =
 
 
 let try_tac tac status =
+ let try_tac status =
   try
     tac status
   with NTacStatus.Error _ ->
     status
+ in
+  atomic_tac try_tac status
 ;;
 
 let first_tac tacl status =
@@ -473,29 +476,24 @@ type indtyinfo = {
         rightno: int;
         leftno: int;
         consno: int;
-        lefts: NCic.term list;
-        rights: NCic.term list;
         reference: NReference.reference;
-        term: NCic.term
  }
 ;;
 
 let ref_of_indtyinfo iti = iti.reference;;
 
 let analyze_indty_tac ~what indtyref =
- distribute_tac (fun status goal ->
+ distribute_tac (fun (status as orig_status) goal ->
   let goalty = get_goalty status goal in
   let status, what = disambiguate status (ctx_of goalty) what None in
   let status, ty_what = typeof status (ctx_of what) what in 
   let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
   let leftno = List.length lefts in
   let rightno = List.length rights in
-  let status,what = term_of_cic_term status what (ctx_of goalty) in
   indtyref := Some { 
-    rightno = rightno; leftno = leftno; consno = consno;
-    lefts = lefts; rights = rights; reference = r; term = what
+    rightno = rightno; leftno = leftno; consno = consno; reference = r;
   };
-  exec id_tac status goal)
+  exec id_tac orig_status goal)
 ;;
 
 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
@@ -525,8 +523,8 @@ let elim_tac ~what:(txt,len,what) ~where =
           (match !sort with NCic.Sort x -> x | _ -> assert false))
      in
      let eliminator = 
-       let what = (HExtlib.unopt !indtyinfo).term in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
+       let _,_,w = what in
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;
@@ -597,13 +595,9 @@ let cases_tac ~what:(txt,len,what) ~where =
   atomic_tac 
    (block_tac [
       analyze_indty_tac ~what indtyinfo;
-      (fun s ->
-        select_tac 
-         ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true
-         s);
-      (fun s ->
-        distribute_tac
-         (cases ~what:("",0,Ast.NCic (HExtlib.unopt !indtyinfo).term)) s); ])
+      (fun s -> select_tac 
+       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
+      distribute_tac (cases ~what) ])
 ;;
 
 let case1_tac name =
@@ -696,8 +690,8 @@ let inversion_tac ~what:(txt,len,what) ~where =
           (match !sort with NCic.Sort x -> x | _ -> assert false))
      in
      let eliminator = 
-       let what = (HExtlib.unopt !indtyinfo).term in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
+       let _,_,w = what in
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;