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 = proof in
+ let uri,metasenv,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' in
+ let newproof = uri,metasenv'',bo',ty', attrs in
(newproof, metasenv'')
(*CSC: commento vecchio *)
(*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) = proof in
+ let (uri,_,bo,ty, attrs) = proof 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' in
+ let newproof = uri,metasenv',bo',ty', attrs in
(newproof, metasenv')
let compare_metasenvs ~oldmetasenv ~newmetasenv =