Back-portin from new Matita: semantics of ntry changed (fixed?) when applied

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index f3d74050f9247cb07cc14d231428c5108ba683da..29683eea5c721f412b08e9c7ba584862bcade754 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/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 =
@@ -371,7 +374,7 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
    let status, instance = 
      mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
    in
-   instantiate status goal instance)
+   instantiate ~refine:false status goal instance)
 ;;
 
 let select_tac ~where ~job move_down_hyps = 
@@ -420,12 +423,12 @@ let generalize_tac ~where =
 ;;
 
 let cut_tac t = 
- block_tac [ 
+ atomic_tac (block_tac [ 
   exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
   branch_tac;
    pos_tac [3]; exact_tac t;
    shift_tac; pos_tac [2]; skip_tac;
-  merge_tac ]
+  merge_tac ])
 ;;
 
 let lapply_tac (s,n,t) = 
@@ -476,6 +479,7 @@ type indtyinfo = {
         lefts: NCic.term list;
         rights: NCic.term list;
         reference: NReference.reference;
+        term: NCic.term
  }
 ;;
 
@@ -489,9 +493,10 @@ let analyze_indty_tac ~what indtyref =
   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;
+    lefts = lefts; rights = rights; reference = r; term = what
   };
   exec id_tac status goal)
 ;;
@@ -523,8 +528,8 @@ let elim_tac ~what:(txt,len,what) ~where =
           (match !sort with NCic.Sort x -> x | _ -> assert false))
      in
      let eliminator = 
-       let _,_,w = what in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+       let what = (HExtlib.unopt !indtyinfo).term in
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;
@@ -540,6 +545,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
      `LeftToRight -> "eq" ^ suffix ^ "_r"
    | `RightToLeft -> "eq" ^ suffix
  in
+ let what = Ast.Appl [what; Ast.Implicit `Vector] in
   block_tac
    [ select_tac ~where ~job:(`Substexpand 2) true;
      exact_tac
@@ -594,9 +600,13 @@ 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);
-      distribute_tac (cases ~what) ])
+      (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); ])
 ;;
 
 let case1_tac name =
@@ -689,8 +699,8 @@ let inversion_tac ~what:(txt,len,what) ~where =
           (match !sort with NCic.Sort x -> x | _ -> assert false))
      in
      let eliminator = 
-       let _,_,w = what in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+       let what = (HExtlib.unopt !indtyinfo).term in
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;