short names

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 422a1be41fdcf3ee6ac58d18183f19dfa1f809de..d8e92cbad4172b6b3064d3ac4f9867851a1283c0 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -38,10 +38,10 @@ let auto_paramod ~params:(l,_) status goal =
   match
     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
   with
-  | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
+  | [] -> raise (Error (lazy "no proof found",None))
   | (pt, metasenv, subst)::_ -> 
       let status = status#set_obj (n,h,metasenv,subst,o) in
-      instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
+      instantiate status goal (mk_cic_term (ctx_of gty) pt)
 ;;
 
 let auto_paramod_tac ~params status = 
@@ -935,7 +935,7 @@ type cache_examination_result =
 
 type sort = T | P
 type goal = int * int * sort (* goal, depth, sort *)
-type fail = goal * NTacStatus.cic_term
+type fail = goal * cic_term
 type candidate = int * NCic.term (* unique candidate number, candidate *)
 
 type op = 
@@ -943,11 +943,11 @@ type op =
   | D of goal 
   (* goal has to be cached as a success obtained using candidate as the first
    * step *)
-  | S of goal * NTacStatus.cic_term * candidate (* int was minsize *)
+  | S of goal * cic_term * candidate (* int was minsize *)
 type 'a elem = 
   (* menv, subst, size, operations done (only S), operations to do, 
    * failures to cache if any op fails *)
-  (#NTacStatus.tac_status as 'a) * int * op list * op list * fail list 
+  (#tac_status as 'a) * int * op list * op list * fail list 
 
 type 'a auto_status = 
   (* list of computations that may lead to the solution: all op list will
@@ -956,7 +956,7 @@ type 'a auto_status =
 
 type 'a auto_result = 
   | Gaveup 
-  | Proved of (#NTacStatus.tac_status as 'a) * 'a auto_status (* alt. proofs *)
+  | Proved of (#tac_status as 'a) * 'a auto_status (* alt. proofs *)
 
 type flags = {
         do_types : bool; (* solve goals in Type *)
@@ -985,21 +985,21 @@ let try_candidate status t g =
    let ast_for_t = 
      match t with
      | NCic.Rel i -> assert false
-     | NCic.Const ref -> CicNotationPt.NRef ref
+     | NCic.Const ref -> Ast.NRef ref
      | _ -> assert false
    in
    let status = NTactics.focus_tac [g] status in
    let status = NTactics.apply_tac ("",0,ast_for_t) status in
-   let open_goals = Continuationals.Stack.head_goals status#stack in
+   let open_goals = head_goals status#stack in
    incr candidate_no;
    Some ((!candidate_no,t),status,open_goals)
- with NTacStatus.Error (msg,exn) -> debug_print msg; None
+ with Error (msg,exn) -> debug_print msg; None
 ;;
 
 
 let get_candidates status context gty =
   let universe = status#auto_cache in
-  let _, gty = NTacStatus.term_of_cic_term status gty (NTacStatus.ctx_of gty) in
+  let _, gty = term_of_cic_term status gty (ctx_of gty) in
   let cands = 
     NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
   in
@@ -1061,8 +1061,8 @@ let equational_and_applicative_case
 ;;
 
 let calculate_goal_ty (goalno,_,_) status = 
-  try Some (NTacStatus.get_goalty status goalno)
-  with NTacStatus.Error _ -> None
+  try Some (get_goalty status goalno)
+  with Error _ -> None
 ;;
 let d_goals l =
   let rec aux acc = function
@@ -1100,7 +1100,6 @@ let auto_main context flags signature elems cache =
           aux tables flags cache elems)
 *)
     | [] ->
-        (* complete failure *)
         debug_print (lazy "gave up");
         Gaveup
     | (s, _, _, [],_)::orlist ->
@@ -1137,7 +1136,7 @@ let auto_main context flags signature elems cache =
             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
             aux ((s,size,don,todo, fl)::orlist, cache)
         | Some gty ->
-            debug_print (lazy ("EXAMINE: "^ NTacStatus.ppterm s gty));
+            debug_print (lazy ("EXAMINE: "^ ppterm s gty));
             match cache_examine cache gty with
             | `Failed_in d when d >= depth -> 
                 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
@@ -1162,7 +1161,7 @@ let auto_main context flags signature elems cache =
                     let cache = cache_add_underinspection cache gty depth in
                     debug_print (lazy ("INSPECTING: " ^ 
                         string_of_int gno ^ "("^ string_of_int size ^ "): "^
-                        NTacStatus.ppterm s gty));
+                        ppterm s gty));
                     (* elems are possible computations for proving gty *)
                     let elems =
                       equational_and_applicative_case 
@@ -1206,15 +1205,8 @@ let auto_main context flags signature elems cache =
 ;;
 
 let auto_tac ~params status =
-  prerr_endline "I teoremi noti sono";
-  NDiscriminationTree.DiscriminationTree.iter status#auto_cache
-    (fun _ t -> 
-      List.iter 
-        (fun t -> 
-           prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
-        (NDiscriminationTree.TermSet.elements t));
   let cache = Cache.empty in
-  let goals = Continuationals.Stack.head_goals status#stack in
+  let goals = head_goals status#stack in
   let depth = 3 in (* XXX fix sort *)
   let goals = List.map (fun i -> D(i,depth,P)) goals in
   let elems = [status,0,[],goals,[]] in
@@ -1227,7 +1219,7 @@ let auto_tac ~params status =
           do_types = false; 
   } in
   match auto_main context flags signature elems cache with
-  | Gaveup -> raise (NTacStatus.Error (lazy "auto gave up", None))
+  | Gaveup -> raise (Error (lazy "auto gave up", None))
   | Proved (s, (_orlist, _cache)) -> 
       let stack = 
         match s#stack with