- let context,name_context = ppcontext' ~sep:"; " subst c in
+ let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
sprintf "%s |- ?%d: %s" context i
sprintf "%s |- ?%d: %s" context i
- (ppterm_in_name_context subst t name_context))
+ (ppterm_in_name_context ~metasenv subst t name_context))
(List.filter
(fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv))
(List.filter
(fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv))
@@ -584,7+586,7 @@ let rec restrict subst to_be_restricted metasenv =
let error_msg = lazy (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
n (names_of_context_indexes context to_be_restricted) n
let error_msg = lazy (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
n (names_of_context_indexes context to_be_restricted) n
- (ppterm subst term))
+ (ppterm ~metasenv subst term))
in
(* DEBUG
debug_print (lazy error_msg);
in
(* DEBUG
debug_print (lazy error_msg);
@@ -658,7+660,7 @@ let delift n subst context metasenv l t =
if (i = n) then
raise (MetaSubstFailure (lazy (sprintf
"Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
if (i = n) then
raise (MetaSubstFailure (lazy (sprintf
"Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
- i (ppterm subst t))))
+ i (ppterm ~metasenv subst t))))
else
begin
(* I do not consider the term associated to ?i in subst since *)
else
begin
(* I do not consider the term associated to ?i in subst since *)