select0_tac ~where ~job:(`ChangeWith change)
;;
+let letin_tac ~where:(_,_,(m,hyp,gp)) ~what:(_,_,w) name =
+ assert(m = None);
+ let where = Some w, [],
+ match gp with
+ | None -> Some Ast.Implicit
+ | Some where ->
+ Some
+ (List.fold_left
+ (fun t _ ->
+ Ast.Binder(`Pi,(Ast.Ident("_",None),Some Ast.UserInput),t))
+ where hyp)
+ in
+ block_tac [
+ generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyp);
+ exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
+ change_tac ~where:("",0,where) ~with_what:("",0,Ast.Ident (name,None))
+ ]
+;;
+
let apply_tac = exact_tac;;
type indtyinfo = {
~what:("",0,Ast.Ident (name,None));
if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
;;
+
+let assert_tac (hyps,concl) = distribute_tac (fun status goal ->
+ let gty = get_goalty status goal in
+ let status,concl = disambiguate status concl None (ctx_of gty) in
+ let status,concl = term_of_cic_term status concl (ctx_of gty) in
+ let status,gty' = term_of_cic_term status gty (ctx_of gty) in
+ assert (concl=gty');
+ let status,_ =
+ List.fold_right2
+ (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
+ assert (id1=id2);
+ match e1,e2 with
+ `Decl t1, NCic.Decl t2 ->
+ let status,t1 = disambiguate status t1 None ctx in
+ let status,t1 = apply_subst status ctx t1 in
+ let status,t1 = term_of_cic_term status t1 ctx in
+ let t2 = mk_cic_term ctx t2 in
+ let status,t2 = apply_subst status ctx t2 in
+ let status,t2 = term_of_cic_term status t2 ctx in
+ assert (t1=t2);
+ status,item::ctx
+ | `Def (b1,t1), NCic.Def (b2,t2) ->
+ let status,t1 = disambiguate status t1 None ctx in
+ let status,t1 = apply_subst status ctx t1 in
+ let status,t1 = term_of_cic_term status t1 ctx in
+ let status,b1 = disambiguate status b1 None ctx in
+ let status,b1 = apply_subst status ctx b1 in
+ let status,b1 = term_of_cic_term status b1 ctx in
+ let t2 = mk_cic_term ctx t2 in
+ let status,t2 = apply_subst status ctx t2 in
+ let status,t2 = term_of_cic_term status t2 ctx in
+ let b2 = mk_cic_term ctx b2 in
+ let status,b2 = apply_subst status ctx b2 in
+ let status,b2 = term_of_cic_term status b2 ctx in
+ assert (t1=t2 && b1=b2);
+ status,item::ctx
+ | _ -> assert false
+ ) hyps (ctx_of gty) (status,[])
+ in
+ exec id_tac status goal)
+;;