arithmetics for λδ

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

diff --git a/matitaB/components/ng_tactics/nTactics.ml b/matitaB/components/ng_tactics/nTactics.ml
index dbc134319424b94f1397903077ebc1e38e68772c..889b8b309c76ab528d4bc8b8a2370a24c869b26b 100644 (file)
--- a/matitaB/components/ng_tactics/nTactics.ml
+++ b/matitaB/components/ng_tactics/nTactics.ml
@@ -205,9 +205,10 @@ let compare_statuses ~past ~present =
 (* CSC: potential bug here: the new methods still use the instance variables
    of the old status and not the instance variables of the new one *)
 let change_stack_type (status : 'a #NTacStatus.status) (stack: 'b) : 'b NTacStatus.status =
+ let uid = status#user in
  let o =
   object
-   inherit ['b] NTacStatus.status status#obj stack
+   inherit ['b] NTacStatus.status uid status#obj stack
    method ppterm = status#ppterm
    method ppcontext = status#ppcontext
    method ppsubst = status#ppsubst
@@ -303,7 +304,7 @@ let assumption_tac status = distribute_tac (fun status goal ->
   let context = ctx_of gty in
   let htac = 
    first_tac
-    (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,None))))
+    (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,`Ambiguous))))
       context)
   in
     exec htac status goal) status
@@ -402,11 +403,11 @@ let select_tac ~where:((txt,txtlen,(wanted,hyps,path)) as where) ~job
   let path = 
    List.fold_left
     (fun path (name,ty) ->
-      NotationPt.Binder (`Forall, (NotationPt.Ident (name,None),Some ty),path))
+      NotationPt.Binder (`Forall, (NotationPt.Ident (name,`Ambiguous),Some ty),path))
     (match path with Some x -> x | None -> NotationPt.UserInput) (List.rev hyps)
   in
    block_tac [ 
-     generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
+     generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,`Ambiguous)) hyps);
      select0_tac ~where:(txt,txtlen,(wanted,[],Some path)) ~job;
      clear_tac (List.map fst hyps) ]
 ;;
@@ -477,7 +478,7 @@ let letin_tac ~where ~what:(_,_,w) name =
  block_tac [
   select_tac ~where ~job:(`Substexpand 1) true;
   exact_tac
-   ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
+   ("",0,Ast.LetIn((Ast.Ident (name,`Ambiguous),None),w,Ast.Implicit `JustOne));
  ]
 ;;
 
@@ -538,7 +539,7 @@ let elim_tac ~what:(txt,len,what) ~where =
      in
      let eliminator = 
        let _,_,w = what in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+       Ast.Appl [ Ast.Ident (name,`Ambiguous) ; Ast.Implicit `Vector ; w ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;
@@ -559,7 +560,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
    [ select_tac ~where ~job:(`Substexpand 2) true;
      exact_tac
       ("",0,
-       Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
+       Ast.Appl(Ast.Ident(name,`Ambiguous)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
         [what]))] status
 ;;
 
@@ -567,7 +568,7 @@ let intro_tac name =
  block_tac
   [ exact_tac
      ("",0,(Ast.Binder (`Lambda,
-      (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
+      (Ast.Ident (name,`Ambiguous),None),Ast.Implicit `JustOne)));
     if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
@@ -619,7 +620,7 @@ let case1_tac name =
  block_tac [ intro_tac name; 
              cases_tac 
               ~where:("",0,(None,[],None)) 
-              ~what:("",0,Ast.Ident (name,None));
+              ~what:("",0,Ast.Ident (name,`Ambiguous));
              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
 
@@ -705,7 +706,7 @@ let inversion_tac ~what:(txt,len,what) ~where =
      in
      let eliminator = 
        let _,_,w = what in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+       Ast.Appl [ Ast.Ident (name,`Ambiguous) ; Ast.Implicit `Vector ; w ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;