+ ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+ ~where:where
+ (* FIXME this is a catch ALL... bad thing *)
+ with exc -> (*prerr_endline (Printexc.to_string exc);*) where
+ in
+ let find_pattern_for name =
+ try Some (snd(List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
+ with Not_found -> None
+ in
+ let ty' =
+ match goal_pattern with
+ | None -> replace context ty [[],ty]
+ | Some pat ->
+ let terms = ProofEngineHelpers.select ~term:ty ~pattern:pat in
+ replace context ty terms
+ in
+ let context' =
+ if hyp_patterns <> [] then
+ List.fold_right
+ (fun entry context ->
+ match entry with
+ | Some (name,Cic.Decl term) ->
+ (match find_pattern_for name with
+ | None -> entry::context
+ | Some pat ->
+ let terms = ProofEngineHelpers.select ~term ~pattern:pat in
+ let where = replace context term terms in
+ let entry = Some (name,Cic.Decl where) in
+ entry::context)
+ | Some (name,Cic.Def (term, None)) ->
+ (match find_pattern_for name with
+ | None -> entry::context
+ | Some pat ->
+ let terms = ProofEngineHelpers.select ~term ~pattern:pat in
+ let where = replace context term terms in
+ let entry = Some (name,Cic.Def (where,None)) in
+ entry::context)
+ | _ -> entry::context
+ ) context []
+ else
+ context
+ in
+ let metasenv' =
+ List.map (function
+ | (n,_,_) when n = metano -> (metano,context',ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ (curi,metasenv',pbo,pty), [metano]