helm/software/components/ng_tactics/nTactics.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 open Printf
  15
  16 let debug = false
  17 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  18
  19 open Continuationals.Stack
  20 open NTacStatus
  21 module Ast = CicNotationPt
  22
  23 let id_tac status = status ;;
  24 let print_tac print_status message status =
  25   if print_status then pp_status status;
  26   prerr_endline message;
  27   status
  28 ;;
  29
  30 let dot_tac status =
  31   let gstatus =
  32     match status#stack with
  33     | [] -> assert false
  34     | ([], _, [], _) :: _ as stack ->
  35         (* backward compatibility: do-nothing-dot *)
  36         stack
  37     | (g, t, k, tag) :: s ->
  38         match filter_open g, k with
  39         | loc :: loc_tl, _ ->
  40              (([ loc ], t, loc_tl @+ k, tag) :: s)
  41         | [], loc :: k ->
  42             assert (is_open loc);
  43             (([ loc ], t, k, tag) :: s)
  44         | _ -> fail (lazy "can't use \".\" here")
  45   in
  46    status#set_stack gstatus
  47 ;;
  48
  49 let branch_tac status =
  50   let gstatus =
  51     match status#stack with
  52     | [] -> assert false
  53     | (g, t, k, tag) :: s ->
  54           match init_pos g with (* TODO *)
  55           | [] | [ _ ] -> fail (lazy "too few goals to branch");
  56           | loc :: loc_tl ->
  57                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
  58   in
  59    status#set_stack gstatus
  60 ;;
  61
  62 let shift_tac status =
  63   let gstatus =
  64     match status#stack with
  65     | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
  66           (match g' with
  67           | [] -> fail (lazy "no more goals to shift")
  68           | loc :: loc_tl ->
  69                 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
  70                 :: (loc_tl, t', k', tag) :: s))
  71      | _ -> fail (lazy "can't shift goals here")
  72   in
  73    status#set_stack gstatus
  74 ;;
  75
  76 let pos_tac i_s status =
  77   let gstatus =
  78     match status#stack with
  79     | [] -> assert false
  80     | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
  81       when is_fresh loc ->
  82         let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
  83           ((l_js, t , [],`BranchTag)
  84            :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
  85     | _ -> fail (lazy "can't use relative positioning here")
  86   in
  87    status#set_stack gstatus
  88 ;;
  89
  90 let wildcard_tac status =
  91   let gstatus =
  92     match status#stack with
  93     | [] -> assert false
  94     | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
  95        when is_fresh loc ->
  96             (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
  97     | _ -> fail (lazy "can't use wildcard here")
  98   in
  99    status#set_stack gstatus
 100 ;;
 101
 102 let merge_tac status =
 103   let gstatus =
 104     match status#stack with
 105     | [] -> assert false
 106     | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
 107         ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
 108     | _ -> fail (lazy "can't merge goals here")
 109   in
 110    status#set_stack gstatus
 111 ;;
 112
 113 let focus_tac gs status =
 114   let gstatus =
 115     match status#stack with
 116     | [] -> assert false
 117     | s -> assert(gs <> []);
 118           let stack_locs =
 119             let add_l acc _ _ l = if is_open l then l :: acc else acc in
 120             fold ~env:add_l ~cont:add_l ~todo:add_l [] s
 121           in
 122           List.iter
 123             (fun g ->
 124               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
 125                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
 126             gs;
 127           (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
 128   in
 129    status#set_stack gstatus
 130 ;;
 131
 132 let unfocus_tac status =
 133   let gstatus =
 134     match status#stack with
 135     | [] -> assert false
 136     | ([], [], [], `FocusTag) :: s -> s
 137     | _ -> fail (lazy "can't unfocus, some goals are still open")
 138   in
 139    status#set_stack gstatus
 140 ;;
 141
 142 let skip_tac status =
 143   let gstatus =
 144     match status#stack with
 145     | [] -> assert false
 146     | (gl, t, k, tag) :: s ->
 147         let gl = List.map switch_of_loc gl in
 148         if List.exists (function Open _ -> true | Closed _ -> false) gl then
 149           fail (lazy "cannot skip an open goal")
 150         else
 151           ([],t,k,tag) :: s
 152   in
 153    status#set_stack gstatus
 154 ;;
 155
 156 let block_tac l status =
 157   List.fold_left (fun status tac -> tac status) status l
 158 ;;
 159
 160
 161 let compare_statuses ~past ~present =
 162  let _,_,past,_,_ = past#obj in
 163  let _,_,present,_,_ = present#obj in
 164  List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
 165  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
 166 ;;
 167
 168
 169
 170 (* Exec and distribute_tac form a retraction pair:
 171     1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
 172     2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
 173          distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
 174     3) tac G = distribute_tac (exec tac) G if
 175        tac = distribute_tac lowtac
 176     4) atomic_tac t === distribute_tac (exec t)
 177
 178    Note that executing an high tactic on a set of goals may be stronger
 179    than executing the same tactic on those goals, but once at a time
 180    (e.g. the tactic could perform a global analysis of the set of goals)
 181 *)
 182
 183 let exec tac (low_status : #lowtac_status) g =
 184   let stack = [ [0,Open g], [], [], `NoTag ] in
 185   let status =
 186    (new NTacStatus.status low_status#obj stack)#set_estatus low_status
 187   in
 188   let status = tac status in
 189    (low_status#set_estatus status)#set_obj status#obj
 190 ;;
 191
 192 let distribute_tac tac (status : #tac_status) =
 193   match status#stack with
 194   | [] -> assert false
 195   | (g, t, k, tag) :: s ->
 196       debug_print (lazy ("context length " ^string_of_int (List.length g)));
 197       let rec aux s go gc =
 198         function
 199         | [] ->
 200             debug_print (lazy "no selected goals");
 201             s, go, gc
 202         | loc :: loc_tl ->
 203             debug_print (lazy "inner eval tactical");
 204             let s, go, gc =
 205               if List.exists ((=) (goal_of_loc loc)) gc then
 206                 s, go, gc
 207               else
 208                 match switch_of_loc loc with
 209                 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
 210                 | Open n ->
 211                    let sn = tac s n in
 212                    let go', gc' = compare_statuses ~past:s ~present:sn in
 213                    sn, ((go @+ [n]) @- gc') @+ go', gc @+ gc'
 214             in
 215             aux s go gc loc_tl
 216       in
 217       let s0 =
 218        (new NTacStatus.status status#obj ())#set_estatus
 219         (status :> NEstatus.status) in
 220       let s0, go0, gc0 = s0, [], [] in
 221       let sn, gon, gcn = aux s0 go0 gc0 g in
 222       debug_print (lazy ("opened: "
 223         ^ String.concat " " (List.map string_of_int gon)));
 224       debug_print (lazy ("closed: "
 225         ^ String.concat " " (List.map string_of_int gcn)));
 226       let stack =
 227         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
 228       in
 229        ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
 230 ;;
 231
 232 let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
 233
 234 let repeat_tac t s =
 235   let rec repeat t (status : #tac_status as 'a) : 'a =
 236     try repeat t (t status)
 237     with NTacStatus.Error _ -> status
 238   in
 239     atomic_tac (repeat t) s
 240 ;;
 241
 242
 243 let try_tac tac status =
 244   try
 245     tac status
 246   with NTacStatus.Error _ ->
 247     status
 248 ;;
 249
 250 let first_tac tacl status =
 251   let res =
 252    HExtlib.list_findopt
 253     (fun tac _ -> try Some (tac status) with NTacStatus.Error _ -> None) tacl
 254   in
 255     match res with
 256       | None -> fail (lazy "No tactics left")
 257       | Some x -> x
 258 ;;
 259
 260 let exact_tac t : 's tactic = distribute_tac (fun status goal ->
 261  let goalty = get_goalty status goal in
 262  let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
 263  instantiate status goal t)
 264 ;;
 265
 266 let assumption_tac status = distribute_tac (fun status goal ->
 267   let gty = get_goalty status goal in
 268   let context = ctx_of gty in
 269   let htac =
 270    first_tac
 271     (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,None))))
 272       context)
 273   in
 274     exec htac status goal) status
 275 ;;
 276
 277 let find_in_context name context =
 278   let rec aux acc = function
 279     | [] -> raise Not_found
 280     | (hd,_) :: tl when hd = name -> acc
 281     | _ :: tl ->  aux (acc + 1) tl
 282   in
 283   aux 1 context
 284 ;;
 285
 286 let clear_tac names =
 287  if names = [] then id_tac
 288  else
 289   distribute_tac (fun status goal ->
 290    let goalty = get_goalty status goal in
 291    let js =
 292      List.map
 293      (fun name ->
 294         try find_in_context name (ctx_of goalty)
 295         with Not_found ->
 296           fail (lazy ("hypothesis '" ^ name ^ "' not found")))
 297      names
 298    in
 299    let n,h,metasenv,subst,o = status#obj in
 300    let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
 301     status#set_obj (n,h,metasenv,subst,o))
 302 ;;
 303
 304 let generalize0_tac args =
 305  if args = [] then id_tac
 306  else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
 307 ;;
 308
 309 let select0_tac ~where:(wanted,hyps,where) ~job  =
 310  let found, postprocess =
 311    match job with
 312    | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
 313    | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1
 314    | `ChangeWith f -> f,(fun s t -> s, t)
 315  in
 316  distribute_tac (fun status goal ->
 317    let goalty = get_goalty status goal in
 318    let path =
 319      match where with None -> NCic.Implicit `Term | Some where -> where
 320    in
 321    let status, newgoalctx =
 322       List.fold_right
 323        (fun (name,d as entry) (status,ctx) ->
 324          try
 325           let path = List.assoc name hyps in
 326            match d with
 327               NCic.Decl ty ->
 328                let status,ty =
 329                 select_term status ~found ~postprocess (mk_cic_term ctx ty)
 330                  (wanted,path) in
 331                let status,ty = term_of_cic_term status ty ctx in
 332                 status,(name,NCic.Decl ty)::ctx
 333             | NCic.Def (bo,ty) ->
 334                let status,bo =
 335                 select_term status ~found ~postprocess (mk_cic_term ctx bo)
 336                  (wanted,path) in
 337                let status,bo = term_of_cic_term status bo ctx in
 338                 status,(name,NCic.Def (bo,ty))::ctx
 339          with
 340           Not_found -> status, entry::ctx
 341        ) (ctx_of goalty) (status,[])
 342    in
 343    let status, newgoalty =
 344      select_term status ~found ~postprocess goalty (wanted,path) in
 345    (* WARNING: the next two lines simply change the context of newgoalty
 346       from the old to the new one. Otherwise mk_meta will do that herself,
 347       calling relocate that calls delift. However, newgoalty is now
 348       ?[out_scope] and thus the delift would trigger the special unification
 349       case, which is wrong now :-( *)
 350    let status,newgoalty = term_of_cic_term status newgoalty (ctx_of goalty) in
 351    let newgoalty = mk_cic_term newgoalctx newgoalty in
 352
 353    let status, instance =
 354      mk_meta status newgoalctx (`Decl newgoalty)
 355    in
 356    instantiate status goal instance)
 357 ;;
 358
 359 let select_tac ~where ~job move_down_hyps =
 360  let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
 361  let path =
 362   match where with None -> NCic.Implicit `Term | Some where -> where in
 363  if not move_down_hyps then
 364   select0_tac ~where:(wanted,hyps,Some path) ~job
 365  else
 366   let path =
 367    List.fold_left
 368      (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
 369      path (List.rev hyps)
 370   in
 371    block_tac [
 372      generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
 373      select0_tac ~where:(wanted,[],Some path) ~job;
 374      clear_tac (List.map fst hyps) ]
 375 ;;
 376
 377 let generalize_tac ~where =
 378  let l = ref [] in
 379  block_tac [
 380    select_tac ~where ~job:(`Collect l) true;
 381    print_tac true "ha selezionato?";
 382    (fun s -> distribute_tac (fun status goal ->
 383       let goalty = get_goalty status goal in
 384       let status,canon,rest =
 385        match !l with
 386           [] ->
 387            (match where with
 388                _,_,(None,_,_)  -> fail (lazy "No term to generalize")
 389              | txt,txtlen,(Some what,_,_) ->
 390                 let status, what =
 391                  disambiguate status (txt,txtlen,what) None (ctx_of goalty)
 392                 in
 393                  status,what,[]
 394            )
 395         | he::tl -> status,he,tl in
 396       let status =
 397        List.fold_left
 398          (fun s t -> unify s (ctx_of goalty) canon t) status rest in
 399       let status, canon = term_of_cic_term status canon (ctx_of goalty) in
 400       instantiate status goal
 401        (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
 402    ) s) ]
 403 ;;
 404
 405 let reduce_tac ~reduction ~where =
 406   let change status t =
 407     match reduction with
 408     | `Normalize perform_delta ->
 409         normalize status
 410          ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
 411     | `Whd perform_delta ->
 412         whd status
 413          ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
 414   in
 415   let where = GrafiteDisambiguate.disambiguate_npattern where in
 416   select0_tac ~where ~job:(`ChangeWith change)
 417 ;;
 418
 419 let change_tac ~where ~with_what =
 420   let change status t =
 421     let status, ww = disambiguate status with_what  None (ctx_of t) in
 422     let status = unify status (ctx_of t) t ww in
 423     status, ww
 424   in
 425   let where = GrafiteDisambiguate.disambiguate_npattern where in
 426   select0_tac ~where ~job:(`ChangeWith change)
 427 ;;
 428
 429 let letin_tac ~where ~what:(_,_,w) name =
 430  block_tac [
 431   select_tac ~where ~job:(`Substexpand 1) true;
 432   exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
 433  ]
 434 ;;
 435
 436 let apply_tac = exact_tac;;
 437
 438 type indtyinfo = {
 439         rightno: int;
 440         leftno: int;
 441         consno: int;
 442         lefts: NCic.term list;
 443         rights: NCic.term list;
 444         reference: NReference.reference;
 445  }
 446 ;;
 447
 448 let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
 449   let goalty = get_goalty status goal in
 450   let status, what = disambiguate status what None (ctx_of goalty) in
 451   let status, ty_what = typeof status (ctx_of what) what in
 452   let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
 453   let leftno = List.length rights in
 454   let rightno = List.length rights in
 455   indtyref := Some {
 456     rightno = rightno; leftno = leftno; consno = consno;
 457     lefts = lefts; rights = rights; reference = r;
 458   };
 459   exec id_tac status goal)
 460 ;;
 461
 462 let elim_tac ~what ~where =
 463   let indtyinfo = ref None in
 464   let sort = ref None in
 465   let compute_goal_sort_tac = distribute_tac (fun status goal ->
 466     let goalty = get_goalty status goal in
 467     let status, goalsort = typeof status (ctx_of goalty) goalty in
 468     sort := Some goalsort;
 469     exec id_tac status goal)
 470   in
 471   atomic_tac (block_tac [
 472     analyze_indty_tac ~what indtyinfo;
 473     (fun s -> select_tac
 474       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
 475     compute_goal_sort_tac;
 476     (fun status ->
 477      let sort = HExtlib.unopt !sort in
 478      let ity = HExtlib.unopt !indtyinfo in
 479      let NReference.Ref (uri, _) = ity.reference in
 480      let status, sort = term_of_cic_term status sort (ctx_of sort) in
 481      let name = NUri.name_of_uri uri ^
 482       match sort with
 483        | NCic.Sort NCic.Prop -> "_ind"
 484        | NCic.Sort _ -> "_rect"
 485        | _ -> assert false
 486      in
 487      let holes =
 488        HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
 489      let eliminator =
 490        let _,_,w = what in
 491        Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
 492      in
 493      exact_tac ("",0,eliminator) status) ])
 494 ;;
 495
 496 let rewrite_tac ~dir ~what:(_,_,what) ~where =
 497  let name =
 498   match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"
 499  in
 500   block_tac
 501    [ select_tac ~where ~job:(`Substexpand 1) true;
 502      exact_tac
 503       ("",0,
 504        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
 505         [what]))]
 506 ;;
 507
 508 let intro_tac name =
 509  block_tac
 510   [ exact_tac
 511      ("",0,(Ast.Binder (`Lambda,
 512       (Ast.Ident (name,None),None),Ast.Implicit)));
 513     if name = "_" then clear_tac [name] else id_tac ]
 514 ;;
 515
 516 let cases ~what status goal =
 517  let gty = get_goalty status goal in
 518  let status, what = disambiguate status what None (ctx_of gty) in
 519  let status, ty = typeof status (ctx_of what) what in
 520  let status, (ref, consno, _, _) = analyse_indty status ty in
 521  let status, what = term_of_cic_term status what (ctx_of gty) in
 522  let t =
 523   NCic.Match (ref,NCic.Implicit `Term, what,
 524     HExtlib.mk_list (NCic.Implicit `Term) consno)
 525  in
 526  let ctx = ctx_of gty in
 527  let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in
 528  instantiate status goal t
 529 ;;
 530
 531 let cases_tac ~what ~where =
 532   let indtyinfo = ref None in
 533   atomic_tac
 534    (block_tac [
 535       analyze_indty_tac ~what indtyinfo;
 536       (fun s -> select_tac
 537        ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
 538       distribute_tac (cases ~what) ])
 539 ;;
 540
 541 let case1_tac name =
 542  let name = if name = "_" then "_clearme" else name in
 543  block_tac [ intro_tac name;
 544              cases_tac
 545               ~where:("",0,(None,[],None))
 546               ~what:("",0,Ast.Ident (name,None));
 547              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 548 ;;
 549
 550 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
 551  let gty = get_goalty status goal in
 552  let eq status ctx t1 t2 =
 553   let status,t1 = disambiguate status t1 None ctx in
 554   let status,t1 = apply_subst status ctx t1 in
 555   let status,t1 = term_of_cic_term status t1 ctx in
 556   let t2 = mk_cic_term ctx t2 in
 557   let status,t2 = apply_subst status ctx t2 in
 558   let status,t2 = term_of_cic_term status t2 ctx in
 559   prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
 560   assert (t1=t2);
 561   status
 562  in
 563  let status,gty' = term_of_cic_term status gty (ctx_of gty) in
 564  let status = eq status (ctx_of gty) concl gty' in
 565  let status,_ =
 566   List.fold_right2
 567    (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
 568      assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
 569      match e1,e2 with
 570         `Decl t1, NCic.Decl t2 ->
 571           let status = eq status ctx t1 t2 in
 572           status,item::ctx
 573       | `Def (b1,t1), NCic.Def (b2,t2) ->
 574           let status = eq status ctx t1 t2 in
 575           let status = eq status ctx b1 b2 in
 576           status,item::ctx
 577       | _ -> assert false
 578    ) hyps (ctx_of gty) (status,[])
 579  in
 580   exec id_tac status goal)
 581 ;;
 582
 583 let assert_tac seqs status =
 584  match status#stack with
 585   | [] -> assert false
 586   | (g,_,_,_) :: s ->
 587      assert (List.length g = List.length seqs);
 588      (match seqs with
 589          [] -> id_tac
 590        | [seq] -> assert0_tac seq
 591        | _ ->
 592          block_tac
 593           (branch_tac::
 594           HExtlib.list_concat ~sep:[shift_tac]
 595             (List.map (fun seq -> [assert0_tac seq]) seqs)@
 596           [merge_tac])
 597      ) status
 598 ;;
 599
 600 let auto ~params:(l,_) status goal =
 601   let gty = get_goalty status goal in
 602   let n,h,metasenv,subst,o = status#obj in
 603   let status,t = term_of_cic_term status gty (ctx_of gty) in
 604   let status, l =
 605     List.fold_left
 606       (fun (status, l) t ->
 607         let status, t = disambiguate status t None (ctx_of gty) in
 608         let status, ty = typeof status (ctx_of t) t in
 609         let status, t =  term_of_cic_term status t (ctx_of gty) in
 610         let status, ty = term_of_cic_term status ty (ctx_of ty) in
 611         (status, (t,ty) :: l))
 612       (status,[]) l
 613   in
 614   match
 615     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
 616   with
 617   | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
 618   | (pt, metasenv, subst)::_ ->
 619       let status = status#set_obj (n,h,metasenv,subst,o) in
 620       instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
 621 ;;
 622
 623 let auto_tac ~params status =
 624   distribute_tac (auto ~params) status
 625 ;;
 626