-let intro_case status gno gty depth cache name =
- (* let status = NTactics.focus_tac [gno] status in *)
- let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in
- let open_goals = head_goals status#stack in
- assert (List.length open_goals = 1);
- let open_goal = List.hd open_goals in
- let ngty = get_goalty status open_goal in
- let ctx = ctx_of ngty in
- let t = mk_cic_term ctx (NCic.Rel 1) in
- let status, keys = keys_of_term status t in
- let cache = List.fold_left (add_to_th t) cache keys in
- debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
- incr candidate_no;
- (* XXX compute the sort *)
- [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]],
- cache
+let intro ~depth status (tcache,fcache) name =
+ let status = NTactics.intro_tac name status in
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals = 1);
+ let open_goal = List.hd open_goals in
+ let ngty = get_goalty status open_goal in
+ let ctx = ctx_of ngty in
+ let t = mk_cic_term ctx (NCic.Rel 1) in
+ let status, keys = keys_of_term status t in
+ let tcache = List.fold_left (add_to_th t) tcache keys in
+ debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
+ (* unprovability is not stable w.r.t introduction *)
+ status, (tcache,[])
+;;
+
+let rec intros ~depth status cache =
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals = 1);
+ let open_goal = List.hd open_goals in
+ let gty = get_goalty status open_goal in
+ let _, raw_gty = term_of_cic_term status gty (ctx_of gty) in
+ match raw_gty with
+ | NCic.Prod (name,_,_) ->
+ let status,cache =
+ intro ~depth status cache (guess_name name (ctx_of gty))
+ in intros ~depth status cache
+ | _ -> status, cache, open_goal
+;;
+
+let reduce ~depth status g =
+ let n,h,metasenv,subst,o = status#obj in
+ let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
+ let ty = NCicUntrusted.apply_subst subst ctx ty in
+ let ty' = NCicReduction.whd ~subst ctx ty in
+ if ty = ty' then []
+ else
+ (debug_print ~depth
+ (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty'));
+ let metasenv =
+ (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
+ in
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ incr candidate_no;
+ [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[g,P]])
+;;
+
+let do_something signature flags status g depth gty cache =
+ let l = reduce ~depth status g in
+ let l1,cache =
+ (equational_and_applicative_case
+ signature flags status g depth gty cache)
+ in
+ sort_new_elems (l@l1), cache