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
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