i,canonical_context',(subst_in ty)
) metasenv'
in
- let bo' = subst_in bo in
+ let bo' = lazy (subst_in (Lazy.force 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 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
+ let bo' = lazy (subst_in (Lazy.force bo)) in
(* Metavariables can appear also in the *statement* of the theorem
* since the parser does not reject as statements terms with
* metavariable therein *)