(* 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
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
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) ]
;;
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));
]
;;
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) ])
;;
[ 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
;;
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 ]
;;
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 ]
;;
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) ])
;;