Just to make it compile again.

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index b64ef34f2087457e50dd6330f85436ec70dbcb6b..58f86c89eb4d1d1e42a75128062ece37fc5f0b25 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -225,14 +225,12 @@ let distribute_tac tac status =
 
 let atomic_tac htac = distribute_tac (exec htac) ;;
 
-let exact t status goal =
+let exact_tac t = distribute_tac (fun status goal ->
  let goalty = get_goalty status goal in
  let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
- instantiate status goal t
+ instantiate status goal t)
 ;;
 
-let exact_tac t = distribute_tac (exact t) ;;
-
 let find_in_context name context =
   let rec aux acc = function
     | [] -> raise Not_found
@@ -242,27 +240,26 @@ let find_in_context name context =
   aux 1 context
 ;;
 
-let clear names status goal =
- let goalty = get_goalty status goal in
- let js =
-   List.map 
+let clear_tac names =
+ if names = [] then id_tac
+ else
+  distribute_tac (fun status goal ->
+   let goalty = get_goalty status goal in
+   let js =
+     List.map 
      (fun name -> 
         try find_in_context name (ctx_of goalty)
         with Not_found -> 
           fail (lazy ("hypothesis '" ^ name ^ "' not found"))) 
      names
- in
- let n,h,metasenv,subst,o = status.pstatus in
- let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
-  { status with pstatus = n,h,metasenv,subst,o }
+   in
+   let n,h,metasenv,subst,o = status.pstatus in
+   let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
+    { status with pstatus = n,h,metasenv,subst,o })
 ;;
 
 let force f s = Lazy.force f s;;
 
-let clear_tac names =
- if names = [] then id_tac else distribute_tac (clear names)
-;;
-
 let generalize0_tac args =
  if args = [] then id_tac
  else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
@@ -343,6 +340,7 @@ let reopen status =
 ;;
 
 let change ~where ~with_what status goal =
+assert false; (*
  let goalty = get_goalty status goal in
  let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
  let path = 
@@ -364,13 +362,12 @@ let change ~where ~with_what status goal =
    mk_meta status (ctx_of newgoalty) (`Decl newgoalty) 
  in
  instantiate status goal instance
+*)
 ;;
-
-let apply t status goal = exact t status goal;;
-
-let apply_tac t = distribute_tac (apply t) ;;
 let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;;
 
+let apply_tac = exact_tac;;
+
 type indtyinfo = {
         rightno: int;
         leftno: int;
@@ -392,7 +389,6 @@ let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
     rightno = rightno; leftno = leftno; consno = consno;
     lefts = lefts; rights = rights; reference = r;
   };
-  prerr_endline "FO";
   exec id_tac status goal)
 ;;
 
@@ -402,7 +398,6 @@ let elim_tac ~what ~where =
   let compute_goal_sort_tac = distribute_tac (fun status goal ->
     let goalty = get_goalty status goal in
     let goalsort = typeof status (ctx_of goalty) goalty in
-    prerr_endline "XXXXXXXX";
     sort := Some goalsort;
     exec id_tac status goal)
   in
@@ -410,9 +405,7 @@ let elim_tac ~what ~where =
     analyze_indty_tac ~what indtyinfo;    
     force (lazy (select_tac 
       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true));
-    print_tac "CIAO";
     compute_goal_sort_tac;
-    print_tac "CIAO2";
     force (lazy (
      let sort = HExtlib.unopt !sort in
      let ity = HExtlib.unopt !indtyinfo in
@@ -437,7 +430,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where =
   match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"
  in
   block_tac
-   [ select_tac ~where ~job:(`Substexpand 2) true;
+   [ select_tac ~where ~job:(`Substexpand 1) true;
      exact_tac
       ("",0,
        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
@@ -447,9 +440,9 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where =
 let intro_tac name =
  block_tac
   [ exact_tac
-    ("",0,(Ast.Binder (`Lambda,
-     (Ast.Ident (name,None),None),Ast.Implicit)));
-     if name = "_" then clear_tac [name] else id_tac ]
+     ("",0,(Ast.Binder (`Lambda,
+      (Ast.Ident (name,None),None),Ast.Implicit)));
+    if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
 let cases ~what status goal =