- let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
- let proof'', new_goals' =
- PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
- in
- (* The apply_tactic can have closed some of the new_goals *)
- let patched_new_goals =
- let (_,metasenv''',_subst,_,_,_) = proof'' in
- List.filter
- (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
- new_goals @ new_goals'
- in
- proof'', patched_new_goals
+ let rec first = (* easier than using tacticals *)
+ function
+ | [] -> raise (PET.Fail (lazy ("unable to generate a working outtype")))
+ | outtype::rest ->
+ let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
+ try
+ let refined_term,_,metasenv'',_ =
+ CicRefine.type_of_aux' metasenv' context term_to_refine
+ CicUniv.oblivion_ugraph
+ in
+ let new_goals =
+ ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+ in
+ let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
+ let proof'', new_goals' =
+ PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+ in
+ (* The apply_tactic can have closed some of the new_goals *)
+ let patched_new_goals =
+ let (_,metasenv''',_subst,_,_,_) = proof'' in
+ List.filter
+ (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
+ new_goals @ new_goals'
+ in
+ proof'', patched_new_goals
+ with PET.Fail _ | CicRefine.RefineFailure _ | CicRefine.Uncertain _ -> first rest