CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern
in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
Some (name,Cic.Decl ty')::context', metasenv, ugraph
| Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
let bo', metasenv, ugraph =
- change subst bo selected_bo metasenv ugraph
- in
+ change subst bo selected_bo metasenv ugraph in
let ty', metasenv, ugraph =
- match ty,selected_ty with
- None,None -> None, metasenv, ugraph
- | Some ty,Some selected_ty ->
- let ty', metasenv, ugraph =
- change subst ty selected_ty metasenv ugraph
- in
- Some ty', metasenv, ugraph
- | _,_ -> assert false
+ change subst ty selected_ty metasenv ugraph
in
(Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
| _,_ -> assert false
| Some lazy_term ->
(fun context metasenv ugraph ->
let what, metasenv, ugraph = lazy_term context metasenv ugraph in
- ProofEngineReduction.unfold ~what, metasenv, ugraph)
+ let unfold ctx t =
+ try
+ ProofEngineReduction.unfold ~what ctx t
+ with
+ (* Not what we would like to have; however, this is required
+ right now for the case of a definition in the context:
+ if it works only in the body (or only in the type), that should
+ be accepted *)
+ ProofEngineTypes.Fail _ -> t
+ in
+ unfold, metasenv, ugraph)
in
mk_tactic (reduction_tac ~reduction ~pattern)
CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture
~pattern in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
let context', metasenv, ugraph =
(Some (name,Cic.Decl ty')::context'), metasenv, ugraph
| Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
let bo', metasenv, ugraph =
- change subst bo selected_bo metasenv ugraph
- in
+ change subst bo selected_bo metasenv ugraph in
let ty', metasenv, ugraph =
- match ty,selected_ty with
- None,None -> None, metasenv, ugraph
- | Some ty,Some selected_ty ->
- let ty', metasenv, ugraph =
- change subst ty selected_ty metasenv ugraph
- in
- Some ty', metasenv, ugraph
- | _,_ -> assert false
+ change subst ty selected_ty metasenv ugraph
in
(Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
| _,_ -> assert false