let reduction_tac ~reduction ~pattern
(proof,goal)
=
let curi,metasenv,pbo,pty = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let reduction_tac ~reduction ~pattern
(proof,goal)
=
let curi,metasenv,pbo,pty = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
~where:where in
let (selected_context,selected_ty) =
ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
~where:where in
let (selected_context,selected_ty) =
ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
let context' =
List.fold_right2
(fun entry selected_entry context' ->
match entry,selected_entry with
None,None -> None::context'
| Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
let context' =
List.fold_right2
(fun entry selected_entry context' ->
match entry,selected_entry with
None,None -> None::context'
| Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
Some (name,Cic.Decl ty')::context'
| Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
Some (name,Cic.Decl ty')::context'
| Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->