+let solve_narrowing bag status active passive goal_steps =
+ let proof, goalno = status in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+ let cleaned_goal = Utils.remove_local_context type_of_goal in
+ let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in
+ let canonical_menv,other_menv =
+ List.partition (fun (_,c,_) -> c = context) metasenv in
+ let canonical_menv =
+ List.map
+ (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv
+ in
+ let metasenv' =
+ List.filter
+ (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal)
+ canonical_menv
+ in
+ let goal = [], metasenv', cleaned_goal in
+ let env = metasenv,context,CicUniv.empty_ugraph in
+ let goals =
+ let table = List.fold_left Indexing.index (last passive) (fst active) in
+ goal :: Indexing.demodulation_all_goal bag env table goal 4
+ in
+ let rec aux newactives newpassives bag = function
+ | [] -> bag, (newactives, newpassives)
+ | hd::tl ->
+ let selected = hd in
+ let (_,m1,t1) = selected in
+ let already_in =
+ List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
+ newactives
+ in
+ if already_in then
+ aux newactives newpassives bag tl
+ else
+ let bag, newpassives =
+ if Utils.metas_of_term t1 = [] then
+ bag, newpassives
+ else
+ let bag, new' =
+ Indexing.superposition_left bag env (snd active) selected
+ in
+ let new' =
+ List.map
+ (fun x -> let b, x = simplify_goal bag env x active in x)
+ new'
+ in
+ bag, newpassives @ new'
+ in
+ aux (selected::newactives) newpassives bag tl
+ in
+ let rec do_n bag ag pg = function
+ | 0 -> None, active, passive, bag
+ | n ->
+ let bag, (ag, pg) = aux [] [] bag (ag @ pg) in
+ match check_if_goals_set_is_solved bag env active passive (ag,pg) with
+ | bag, None -> do_n bag ag pg (n-1)
+ | bag, Some (gproof,newproof,subsumption_id,subsumption_subst,pmenv)->
+ let subst, proof, gl =
+ build_proof bag
+ status gproof newproof subsumption_id subsumption_subst pmenv
+ in
+ let uri,metasenv,subst,meta_proof,term_to_prove,attrs = proof in
+ let proof =
+ uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs
+ in
+ Some (subst, proof,gl),active,passive, bag
+ in
+ do_n bag [] goals goal_steps
+;;
+