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