exception Bad_pattern of string Lazy.t
-let new_meta_of_proof ~proof:(_, metasenv, _, _, _) =
+let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) =
CicMkImplicit.new_meta metasenv []
let subst_meta_in_proof proof meta term newmetasenv =
- let uri,metasenv,bo,ty, attrs = proof in
+ let uri,metasenv,initial_subst,bo,ty, attrs = proof in
(* empty context is ok for term since it wont be used by apply_subst *)
(* hack: since we do not know the context and the type of term, we
create a substitution with cc =[] and type = Implicit; they will be
* since the parser does not reject as statements terms with
* metavariable therein *)
let ty' = subst_in ty in
- let newproof = uri,metasenv'',bo',ty', attrs in
+ let newproof = uri,metasenv'',initial_subst,bo',ty', attrs in
(newproof, metasenv'')
(*CSC: commento vecchio *)
(*CSC: ci ripasso sopra apply_subst!!! *)
(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
(*CSC: [newmetasenv]. *)
-let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,_,bo,ty, attrs) = proof in
+let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
+ let (uri,_,initial_subst,bo,ty, attrs) = proof in
+ let subst_in = CicMetaSubst.apply_subst subst in
let bo' = subst_in bo in
(* Metavariables can appear also in the *statement* of the theorem
* since the parser does not reject as statements terms with
| _ -> i
) newmetasenv []
in
- let newproof = uri,metasenv',bo',ty', attrs in
+ (* qui da capire se per la fase transitoria si fa initial_subst @ subst
+ * oppure subst *)
+ let newproof = uri,metasenv',subst,bo',ty', attrs in
(newproof, metasenv')
let compare_metasenvs ~oldmetasenv ~newmetasenv =