Matitaweb: first attempt at "Save as".

[helm.git] / matitaB / components / ng_tactics / nnAuto.ml

diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index 020b819c93ac8df0a5388e7de764bc75a6053b2c..9ef663ee11fe12c8ddc398f01592068fb668c060 100644 (file)
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -1136,7 +1136,7 @@ let applicative_case depth signature status flags gty cache =
   let candidates,smart_candidates = 
     let test x = not (is_a_fact_ast status subst metasenv context x) in
     if is_eq then 
-      Ast.Ident("refl",None) ::List.filter test candidates,
+      Ast.Ident("refl",`Ambiguous) ::List.filter test candidates,
       List.filter test smart_candidates
     else candidates,smart_candidates in 
   debug_print ~depth
@@ -1292,12 +1292,12 @@ let intros ~depth status cache =
           in 
           if head_goals status#stack = [] then 
             let status = NTactics.merge_tac status in
-            [(0,Ast.Ident("__intros",None)),status], cache
+            [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
           else
             (* we reindex the equation from scratch *)
             let unit_eq = index_local_equations status#eq_cache status in
             let status = NTactics.merge_tac status in
-            [(0,Ast.Ident("__intros",None)),status], 
+            [(0,Ast.Ident("__intros",`Ambiguous)),status], 
             init_cache ~facts ~unit_eq () ~trace
       | _ -> [],cache
 ;;
@@ -1321,7 +1321,7 @@ let reduce ~whd ~depth status g =
        be empty *)
     let status = NTactics.merge_tac status in
     incr candidate_no;
-    [(!candidate_no,Ast.Ident("__whd",None)),status])
+    [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
 ;;
 
 let do_something signature flags status g depth gty cache =
@@ -1336,7 +1336,7 @@ let do_something signature flags status g depth gty cache =
     List.map 
       (fun s ->
          incr candidate_no;
-         ((!candidate_no,Ast.Ident("__paramod",None)),s))
+         ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
       (auto_eq_check cache.unit_eq status) 
   in
   let l2 = 
@@ -1628,8 +1628,8 @@ auto_main flags signature cache depth status: unit =
              debug_print (~depth:depth) 
                (lazy ("Case: " ^ NotationPp.pp_term status t));
              let depth,cache =
-              if t=Ast.Ident("__whd",None) || 
-                  t=Ast.Ident("__intros",None) 
+              if t=Ast.Ident("__whd",`Ambiguous) || 
+                  t=Ast.Ident("__intros",`Ambiguous) 
                then depth, cache 
               else depth+1,loop_cache in 
             let cache = add_to_trace status ~depth cache t in