*)
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
- CicMkImplicit.new_meta metasenv
+ CicMkImplicit.new_meta metasenv []
let subst_meta_in_proof proof meta term newmetasenv =
let uri,metasenv,bo,ty = proof in
- let subst_in = CicMetaSubst.apply_subst [meta,term] 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
+ in any case dropped by apply_subst, but it would be better to rewrite
+ the code. Cannot we just use apply_subst_metasenv, etc. ?? *)
+ let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in
let metasenv' =
newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
in
) metasenv'
in
let bo' = subst_in bo in
- let newproof = uri,metasenv'',bo',ty in
+ (* Metavariables can appear also in the *statement* of the theorem
+ * 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
(newproof, metasenv'')
(*CSC: commento vecchio *)
let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
let (uri,_,bo,ty) = 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
+ * metavariable therein *)
+ let ty' = subst_in ty in
let metasenv' =
List.fold_right
(fun metasenv_entry i ->
| _ -> i
) newmetasenv []
in
- let newproof = uri,metasenv',bo',ty in
+ let newproof = uri,metasenv',bo',ty' in
(newproof, metasenv')
+let compare_metasenvs ~oldmetasenv ~newmetasenv =
+ List.map (function (i,_,_) -> i)
+ (List.filter
+ (function (i,_,_) ->
+ not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
+;;