-let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) =
- CicMkImplicit.new_meta metasenv []
+let new_meta_of_proof ~proof:(_, metasenv, subst, _, _, _) =
+ CicMkImplicit.new_meta metasenv subst
let subst_meta_in_proof proof meta term newmetasenv =
let uri,metasenv,initial_subst,bo,ty, attrs = proof in
let subst_meta_in_proof proof meta term newmetasenv =
let uri,metasenv,initial_subst,bo,ty, attrs = proof in
let add_ctx context name entry = (Some (name, entry)) :: context in
let map2 error_msg f l1 l2 =
try
let add_ctx context name entry = (Some (name, entry)) :: context in
let map2 error_msg f l1 l2 =
try
- None -> [],metasenv,ugraph,roots
+ None -> subst,metasenv,ugraph,roots
- [] -> [],metasenv,ugraph,[]
+ [] -> subst,metasenv,ugraph,[]
- let subst,metasenv,ugraph,tl' = find_in_roots tl in
+ let subst,metasenv,ugraph,tl' = find_in_roots subst tl in
let subst,metasenv,ugraph,found =
let wanted, metasenv, ugraph = wanted context' metasenv ugraph in
find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context'
let subst,metasenv,ugraph,found =
let wanted, metasenv, ugraph = wanted context' metasenv ugraph in
find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context'
in
subst,metasenv,ugraph,found @ tl'
in
in
subst,metasenv,ugraph,found @ tl'
in
(** create a pattern from a term and a list of subterms.
* the pattern is granted to have a ? for every subterm that has no selected
(** create a pattern from a term and a list of subterms.
* the pattern is granted to have a ? for every subterm that has no selected
~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
=
let what, hyp_patterns, goal_pattern = pattern in
~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
=
let what, hyp_patterns, goal_pattern = pattern in
aux [] context
in
let subst,metasenv,ugraph,ty_terms =
aux [] context
in
let subst,metasenv,ugraph,ty_terms =
- select_in_term ~metasenv ~context ~ugraph ~term:ty
- ~pattern:(what,goal_pattern) in
+ select_in_term ~metasenv ~subst ~context ~ugraph ~term:ty
+ ~pattern:(what,goal_pattern)
+ in
let subst,metasenv,ugraph,context_terms =
let subst,metasenv,ugraph,res,_ =
(List.fold_right
let subst,metasenv,ugraph,context_terms =
let subst,metasenv,ugraph,res,_ =
(List.fold_right
subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
| Some pat ->
let subst,metasenv,ugraph,terms =
subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
| Some pat ->
let subst,metasenv,ugraph,terms =
~pattern:(what, Some pat)
in
subst,metasenv,ugraph,((Some (`Decl terms))::res),
~pattern:(what, Some pat)
in
subst,metasenv,ugraph,((Some (`Decl terms))::res),
(entry::context)
| Some pat ->
let subst,metasenv,ugraph,terms_bo =
(entry::context)
| Some pat ->
let subst,metasenv,ugraph,terms_bo =
~pattern:(what, Some pat) in
let subst,metasenv,ugraph,terms_ty =
let subst,metasenv,ugraph,res =
~pattern:(what, Some pat) in
let subst,metasenv,ugraph,terms_ty =
let subst,metasenv,ugraph,res =
~pattern:(what, Some pat)
in
subst,metasenv,ugraph,res
~pattern:(what, Some pat)
in
subst,metasenv,ugraph,res
subst,metasenv,ugraph,res
in
subst,metasenv,ugraph,context_terms, ty_terms
subst,metasenv,ugraph,res
in
subst,metasenv,ugraph,context_terms, ty_terms
(** locate_in_term equality what where context
* [what] must match a subterm of [where] according to [equality]
(** locate_in_term equality what where context
* [what] must match a subterm of [where] according to [equality]