From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 12 Nov 2006 18:58:56 +0000 (+0000)
Subject: The pretty printers in CicPp now have an optional ~metasenv argument to
X-Git-Tag: 0.4.95@7852~814
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b20889b47bf949b17a6297ac39a5c0df0301de9e;p=helm.git

The pretty printers in CicPp now have an optional ~metasenv argument to
show the globally restricted arguments of a metavariable local context as
locally restricted. The pretty printers in CicMetaSubst have the same argument,
but the argument is mandatory.
---

diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml
index f3560cc3a..55d94899b 100644
--- a/components/cic_proof_checking/cicPp.ml
+++ b/components/cic_proof_checking/cicPp.ml
@@ -62,6 +62,7 @@ let rec get_nth l n =
 (* pretty-prints a term t of cic in an environment l where l is a list of  *)
 (* identifier names used to resolve DeBrujin indexes. The head of l is the *)
 (* name associated to the greatest DeBrujin index in t                     *)
+let pp ?metasenv =
 let rec pp t l =
  let module C = Cic in
    match t with
@@ -79,10 +80,33 @@ let rec pp t l =
     | C.Var (uri,exp_named_subst) ->
        UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
     | C.Meta (n,l1) ->
-       "?" ^ (string_of_int n) ^ "[" ^ 
-        String.concat " ; "
-         (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
-        "]"
+       (match metasenv with
+           None ->
+            "?" ^ (string_of_int n) ^ "[" ^ 
+             String.concat " ; "
+              (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+             "]"
+         | Some metasenv ->
+            try
+             let _,context,_ = CicUtil.lookup_meta n metasenv in
+              "?" ^ (string_of_int n) ^ "[" ^ 
+               String.concat " ; "
+                (List.rev
+                  (List.map2
+                    (fun x y ->
+                      match x,y with
+                         _, None
+                       | None, _ -> "_"
+                       | Some _, Some t -> pp t l
+                    ) context l1)) ^
+               "]"
+            with
+             CicUtil.Meta_not_found _ ->
+              "???" ^ (string_of_int n) ^ "[" ^ 
+               String.concat " ; "
+                (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+               "]"
+       )
     | C.Sort s ->
        (match s with
            C.Prop  -> "Prop"
@@ -223,10 +247,12 @@ and pp_exp_named_subst exp_named_subst l =
      (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l)
      exp_named_subst
    ) ^ "]"
+in
+ pp
 ;;
 
-let ppterm t =
- pp t []
+let ppterm ?metasenv t =
+ pp ?metasenv t []
 ;;
 
 (* ppinductiveType (typename, inductive, arity, cons)                       *)
@@ -241,20 +267,20 @@ let ppinductiveType (typename, inductive, arity, cons) =
    cons ""
 ;;
 
-let ppcontext ?(sep = "\n") context =
+let ppcontext ?metasenv ?(sep = "\n") context =
  let separate s = if s = "" then "" else s ^ sep in
  fst (List.fold_right 
    (fun context_entry (i,name_context) ->
      match context_entry with
         Some (n,Cic.Decl t) ->
          Printf.sprintf "%s%s : %s" (separate i) (ppname n)
-          (pp t name_context), (Some n)::name_context
+          (pp ?metasenv t name_context), (Some n)::name_context
       | Some (n,Cic.Def (bo,ty)) ->
          Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
           (match ty with
               None -> "_"
-            | Some ty -> pp ty name_context)
-          (pp bo name_context), (Some n)::name_context
+            | Some ty -> pp ?metasenv ty name_context)
+          (pp ?metasenv bo name_context), (Some n)::name_context
        | None ->
           Printf.sprintf "%s_ :? _" (separate i), None::name_context
     ) context ("",[]))
@@ -292,11 +318,13 @@ let ppobj obj =
 	            (match context_entry with
 	                Some (n,C.Decl at) ->
                    (separate i) ^
-                     ppname n ^ ":" ^ pp at name_context ^ " ",
+                     ppname n ^ ":" ^
+                      pp ~metasenv:conjectures at name_context ^ " ",
                       (Some n)::name_context
 	              | Some (n,C.Def (at,None)) ->
                    (separate i) ^
-                     ppname n ^ ":= " ^ pp at name_context ^ " ",
+                     ppname n ^ ":= " ^ pp ~metasenv:conjectures
+                      at name_context ^ " ",
                       (Some n)::name_context
                 | None ->
                    (separate i) ^ "_ :? _ ", None::name_context
@@ -304,9 +332,10 @@ let ppobj obj =
             ) context ("",[])
           in
            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
-            pp t name_context ^ "\n" ^ i
+            pp ~metasenv:conjectures t name_context ^ "\n" ^ i
         ) conjectures "" ^
-        "\n" ^ pp value [] ^ " : " ^ pp ty [] 
+        "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^
+          pp ~metasenv:conjectures ty [] 
    | C.InductiveDefinition (l, params, nparams, _) ->
       "Parameters = " ^
        String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
diff --git a/components/cic_proof_checking/cicPp.mli b/components/cic_proof_checking/cicPp.mli
index e84ae4fed..e898c352d 100644
--- a/components/cic_proof_checking/cicPp.mli
+++ b/components/cic_proof_checking/cicPp.mli
@@ -40,13 +40,13 @@
 (* similar to the one used by Coq                                            *)
 val ppobj : Cic.obj -> string
 
-val ppterm : Cic.term -> string
+val ppterm : ?metasenv:Cic.metasenv -> Cic.term -> string
 
-val ppcontext : ?sep:string -> Cic.context -> string 
+val ppcontext : ?metasenv:Cic.metasenv -> ?sep:string -> Cic.context -> string 
 
 (* Required only by the topLevel. It is the generalization of ppterm to *)
 (* work with environments.                                              *)
-val pp : Cic.term -> (Cic.name option) list -> string
+val pp : ?metasenv:Cic.metasenv -> Cic.term -> (Cic.name option) list -> string
 
 val ppname : Cic.name -> string
 
diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml
index 8d53495bf..c097eacf2 100644
--- a/components/cic_unification/cicMetaSubst.ml
+++ b/components/cic_unification/cicMetaSubst.ml
@@ -293,67 +293,70 @@ let apply_subst_metasenv subst metasenv =
 
 (***** Pretty printing functions ******)
 
-let ppterm subst term = CicPp.ppterm (apply_subst subst term)
+let ppterm ~metasenv subst term =
+ CicPp.ppterm ~metasenv (apply_subst subst term)
 
-let ppterm_in_name_context subst term name_context =
- CicPp.pp (apply_subst subst term) name_context
+let ppterm_in_name_context ~metasenv subst term name_context =
+ CicPp.pp ~metasenv (apply_subst subst term) name_context
 
-let ppterm_in_context subst term context =
+let ppterm_in_context ~metasenv subst term context =
  let name_context =
   List.map (function None -> None | Some (n,_) -> Some n) context
  in
-  ppterm_in_name_context subst term name_context
+  ppterm_in_name_context ~metasenv subst term name_context
 
-let ppcontext' ?(sep = "\n") subst context =
+let ppcontext' ~metasenv ?(sep = "\n") subst context =
  let separate s = if s = "" then "" else s ^ sep in
   List.fold_right 
    (fun context_entry (i,name_context) ->
      match context_entry with
         Some (n,Cic.Decl t) ->
          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_name_context subst t name_context), (Some n)::name_context
+          (ppterm_in_name_context ~metasenv subst t name_context),
+          (Some n)::name_context
       | Some (n,Cic.Def (bo,ty)) ->
          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
           (match ty with
               None -> "_"
-            | Some ty -> ppterm_in_name_context subst ty name_context)
-          (ppterm_in_name_context subst bo name_context), (Some n)::name_context
+            | Some ty -> ppterm_in_name_context ~metasenv subst ty name_context)
+          (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context
        | None ->
           sprintf "%s_ :? _" (separate i), None::name_context
     ) context ("",[])
 
-let ppsubst_unfolded subst =
+let ppsubst_unfolded ~metasenv subst =
   String.concat "\n"
     (List.map
       (fun (idx, (c, t,_)) ->
-        let context,name_context = ppcontext' ~sep:"; " subst c in
+        let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
          sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_name_context subst t name_context))
+          (ppterm_in_name_context ~metasenv subst t name_context))
        subst)
 (* 
         Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
       subst) *)
 ;;
 
-let ppsubst subst =
+let ppsubst ~metasenv subst =
   String.concat "\n"
     (List.map
       (fun (idx, (c, t, _)) ->
-        let context,name_context = ppcontext' ~sep:"; " [] c in
+        let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in
          sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_name_context [] t name_context))
+          (ppterm_in_name_context ~metasenv [] t name_context))
        subst)
 ;;
 
-let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
+let ppcontext ~metasenv ?sep subst context =
+ fst (ppcontext' ~metasenv ?sep subst context)
 
 let ppmetasenv ?(sep = "\n") subst metasenv =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
-        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
-          (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))
@@ -583,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
-            (ppterm subst term))
+            (ppterm ~metasenv subst term))
 	  in 
           (* DEBUG
           debug_print (lazy error_msg);
@@ -657,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)"
-              i (ppterm subst t))))
+              i (ppterm ~metasenv subst t))))
           else
             begin
            (* I do not consider the term associated to ?i in subst since *)
@@ -741,10 +744,10 @@ debug_print(lazy (sprintf
           )))); *)
       let msg = (lazy (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
-        (ppterm subst t)
+        (ppterm ~metasenv subst t)
         (String.concat "; "
           (List.map
-            (function Some t -> ppterm subst t | None -> "_")
+            (function Some t -> ppterm ~metasenv subst t | None -> "_")
             l))))
       in
        if
@@ -909,6 +912,6 @@ let fpp_gen ppf s =
   Format.pp_print_newline ppf ();
   Format.pp_print_flush ppf ()
 
-let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
+let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst)
 let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
 let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)
diff --git a/components/cic_unification/cicMetaSubst.mli b/components/cic_unification/cicMetaSubst.mli
index 96f87205f..2b60b04e0 100644
--- a/components/cic_unification/cicMetaSubst.mli
+++ b/components/cic_unification/cicMetaSubst.mli
@@ -61,14 +61,17 @@ val delift_rels :
  
 (** {2 Pretty printers} *)
 
-val ppsubst_unfolded: Cic.substitution -> string
-val ppsubst: Cic.substitution -> string
-val ppterm: Cic.substitution -> Cic.term -> string
-val ppcontext: ?sep: string -> Cic.substitution -> Cic.context -> string
+val ppsubst_unfolded: metasenv:Cic.metasenv -> Cic.substitution -> string
+val ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string
+val ppterm: metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> string
+val ppcontext:
+ metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context ->
+   string
 val ppterm_in_name_context:
- Cic.substitution -> Cic.term -> (Cic.name option) list -> string
+ metasenv:Cic.metasenv -> Cic.substitution -> Cic.term ->
+  (Cic.name option) list -> string
 val ppterm_in_context:
- Cic.substitution -> Cic.term -> Cic.context -> string
+ metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string
 val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string
 
 (** {2 Format-like pretty printers}
diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index e1253f8e8..36347ccd1 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -146,12 +146,12 @@ let is_a_double_coercion t =
   | _ -> dummyres
 
 let more_args_than_expected
-  localization_tbl subst he context hetype' tlbody_and_type exn
+  localization_tbl metasenv subst he context hetype' tlbody_and_type exn
 =
   let msg = 
     lazy ("The term " ^
-      CicMetaSubst.ppterm_in_context subst he context ^ 
-      " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^
+      CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ 
+      " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
       ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
       " arguments that are more than expected")
   in
@@ -427,11 +427,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 enrich localization_tbl te'
                  ~f:(fun _ ->
                    lazy ("The term " ^
-                    CicMetaSubst.ppterm_in_context subst'' te'
+                    CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
                      context ^ " has type " ^
-                    CicMetaSubst.ppterm_in_context subst'' inferredty
+                    CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
                      context ^ " but is here used with type " ^
-                    CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
+                    CicMetaSubst.ppterm_in_context metasenv'' subst'' ty' context)) exn
              )
         | C.Prod (name,s,t) ->
             let carr t subst context = CicMetaSubst.apply_subst subst t in
@@ -460,17 +460,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        enrich localization_tbl t
                         (RefineFailure 
                           (lazy ("The term " ^ 
-                          CicMetaSubst.ppterm_in_context subst t context ^ 
+                          CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
                           " is not a type since it has type " ^ 
-                          CicMetaSubst.ppterm_in_context
+                          CicMetaSubst.ppterm_in_context ~metasenv
                            subst coercion_src context ^ " that is not a sort")))
                     | CoercGraph.NotMetaClosed -> 
                        enrich localization_tbl t
                         (Uncertain 
                           (lazy ("The term " ^ 
-                          CicMetaSubst.ppterm_in_context subst t context ^ 
+                          CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
                           " is not a type since it has type " ^ 
-                          CicMetaSubst.ppterm_in_context 
+                          CicMetaSubst.ppterm_in_context ~metasenv
                            subst coercion_src context ^ " that is not a sort")))
                     | CoercGraph.SomeCoercion candidates -> 
                         let selected = 
@@ -485,10 +485,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                             enrich localization_tbl t
                               (RefineFailure 
                                 (lazy ("The term " ^ 
-                                CicMetaSubst.ppterm_in_context 
+                                CicMetaSubst.ppterm_in_context ~metasenv
                                   subst t context ^ 
                                   " is not a type since it has type " ^ 
-                                  CicMetaSubst.ppterm_in_context
+                                  CicMetaSubst.ppterm_in_context ~metasenv
                                   subst coercion_src context ^ 
                                   " that is not a sort")))) 
             in
@@ -534,17 +534,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                         enrich localization_tbl s'
                          (RefineFailure 
                           (lazy ("The term " ^ 
-                          CicMetaSubst.ppterm_in_context subst s' context ^ 
+                          CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
                           " is not a type since it has type " ^ 
-                          CicMetaSubst.ppterm_in_context 
+                          CicMetaSubst.ppterm_in_context ~metasenv
                            subst coercion_src context ^ " that is not a sort")))
                       | CoercGraph.NotMetaClosed -> 
                         enrich localization_tbl s'
                          (Uncertain 
                           (lazy ("The term " ^ 
-                          CicMetaSubst.ppterm_in_context subst s' context ^ 
+                          CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
                           " is not a type since it has type " ^ 
-                          CicMetaSubst.ppterm_in_context 
+                          CicMetaSubst.ppterm_in_context ~metasenv 
                            subst coercion_src context ^ " that is not a sort")))
                       | CoercGraph.SomeCoercion candidates -> 
                         let selected = 
@@ -559,9 +559,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                            enrich localization_tbl s'
                             (RefineFailure 
                              (lazy ("The term " ^ 
-                              CicMetaSubst.ppterm_in_context subst s' context ^ 
+                              CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
                               " is not a type since it has type " ^ 
-                              CicMetaSubst.ppterm_in_context 
+                              CicMetaSubst.ppterm_in_context ~metasenv
                               subst coercion_src context ^ 
                               " that is not a sort")))
             in
@@ -691,11 +691,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               enrich localization_tbl term' exn
                ~f:(function _ ->
                  lazy ("The term " ^
-                  CicMetaSubst.ppterm_in_context subst term'
+                  CicMetaSubst.ppterm_in_context ~metasenv subst term'
                    context ^ " has type " ^
-                  CicMetaSubst.ppterm_in_context subst actual_type
+                  CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
                    context ^ " but is here used with type " ^
-                  CicMetaSubst.ppterm_in_context subst expected_type' context))
+                  CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
            in
            let rec instantiate_prod t =
             function
@@ -911,11 +911,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        enrich localization_tbl p exn
                         ~f:(function _ ->
                           lazy ("The term " ^
-                           CicMetaSubst.ppterm_in_context subst p
+                           CicMetaSubst.ppterm_in_context ~metasenv subst p
                             context ^ " has type " ^
-                           CicMetaSubst.ppterm_in_context subst instance'
+                           CicMetaSubst.ppterm_in_context ~metasenv subst instance'
                             context ^ " but is here used with type " ^
-                           CicMetaSubst.ppterm_in_context subst instance
+                           CicMetaSubst.ppterm_in_context ~metasenv subst instance
                             context)))
                  (subst,metasenv,ugraph5) pl' outtypeinstances 
              in
@@ -952,11 +952,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
                          lazy ("The term " ^
-                          CicMetaSubst.ppterm_in_context subst bo
+                          CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
-                          CicMetaSubst.ppterm_in_context subst ty_of_bo
+                          CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
                            context' ^ " but is here used with type " ^
-                          CicMetaSubst.ppterm_in_context subst expected_ty
+                          CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
                            context))
                    in 
                      fl @ [bo'] , subst',metasenv',ugraph'
@@ -1005,11 +1005,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
                          lazy ("The term " ^
-                          CicMetaSubst.ppterm_in_context subst bo
+                          CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
-                          CicMetaSubst.ppterm_in_context subst ty_of_bo
+                          CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
                            context' ^ " but is here used with type " ^
-                          CicMetaSubst.ppterm_in_context subst expected_ty
+                          CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
                            context))
                    in
                      fl @ [bo'],subst',metasenv',ugraph'
@@ -1070,7 +1070,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    (try
 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
                       fo_unif_subst subst context metasenv t ct ugraph
-                    with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+                    with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
                    in
                      l @ [Some t],subst',metasenv',ugraph'
                | Some t,Some (_,C.Decl ct) ->
@@ -1081,19 +1081,19 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                      (try
                         fo_unif_subst
                           subst' context metasenv' inferredty ct ugraph1
-                      with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+                      with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
                    in
                      l @ [Some t'], subst'',metasenv'',ugraph2
                | None, Some _  ->
-                   raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context 
+                   raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context 
       with
           Invalid_argument _ ->
             raise
             (RefineFailure
                (lazy (sprintf
                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
-                  (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
-                  (CicMetaSubst.ppcontext subst canonical_context))))
+                  (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
+                  (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
 
   and check_exp_named_subst metasubst metasenv context tl ugraph =
     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
@@ -1126,9 +1126,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               with _ ->
                 raise (RefineFailure (lazy
                          ("Wrong Explicit Named Substitution: " ^ 
-                           CicMetaSubst.ppterm metasubst' typeoft ^
+                           CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
                           " not unifiable with " ^ 
-                          CicMetaSubst.ppterm metasubst' typeofvar)))
+                          CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
             in
             (* FIXME: no mere tail recursive! *)
             let exp_name_subst, metasubst''', metasenv''', ugraph4 = 
@@ -1185,16 +1185,16 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                (lazy 
                  (sprintf
                    "%s is supposed to be a type, but its type is %s"
-               (CicMetaSubst.ppterm_in_context subst t context)
-               (CicMetaSubst.ppterm_in_context subst t2 context))))
+               (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
+               (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
         | _,_ -> 
             enrich localization_tbl t
              (RefineFailure 
                (lazy 
                  (sprintf
                    "%s is supposed to be a type, but its type is %s"
-               (CicMetaSubst.ppterm_in_context subst s context)
-               (CicMetaSubst.ppterm_in_context subst t1 context))))
+               (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
+               (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
 
   and avoid_double_coercion context subst metasenv ugraph t ty = 
    if not !pack_coercions then
@@ -1317,8 +1317,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         (* {{{ we search a coercion of the head (saturated) to funclass *)
         let metasenv = pristinemenv in
         debug_print (lazy 
-          ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
-           " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' 
+          ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
+           " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype' 
            (* ^ " cause: " ^ Lazy.force s *)));
         let how_many_args_are_needed = 
           let rec aux n = function
@@ -1355,7 +1355,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
             HExtlib.list_findopt 
               (fun coerc -> 
                 let t = Cic.Appl [coerc;x] in
-                debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t));
+                debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t));
                 try
                   (* we want this to be available in the error handler fo the
                    * following (so it has its own try. *)
@@ -1367,8 +1367,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                       mk_prod_of_metas metasenv context subst remainder 
                     in
                     debug_print (lazy 
-                      ("  unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^ 
-                       CicMetaSubst.ppterm subst hetype'));
+                      ("  unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^ 
+                       CicMetaSubst.ppterm ~metasenv subst hetype'));
                     let subst,metasenv,ugraph = 
                       fo_unif_subst_eat_prods 
                         subst context metasenv tty hetype' ugraph
@@ -1392,7 +1392,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
            | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
                subst,metasenv,ugraph,hetype',he,args_bo_and_ty
            | None -> 
-               more_args_than_expected localization_tbl 
+               more_args_than_expected localization_tbl metasenv
                  subst he context hetype args_bo_and_ty exn
       (* }}} end coercion to funclass stuff *)           
       (* }}} end fix_arity *)           
@@ -1432,21 +1432,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                         enrich localization_tbl hete exn
                          ~f:(fun _ ->
                            (lazy ("The term " ^
-                             CicMetaSubst.ppterm_in_context subst hete
+                             CicMetaSubst.ppterm_in_context ~metasenv subst hete
                               context ^ " has type " ^
-                             CicMetaSubst.ppterm_in_context subst hety
+                             CicMetaSubst.ppterm_in_context ~metasenv subst hety
                               context ^ " but is here used with type " ^
-                             CicMetaSubst.ppterm_in_context subst s context
+                             CicMetaSubst.ppterm_in_context ~metasenv subst s context
                               (* "\nReason: " ^ Lazy.force e*))))
                     | CoercGraph.NotMetaClosed -> 
                         enrich localization_tbl hete exn
                          ~f:(fun _ ->
                            (lazy ("The term " ^
-                             CicMetaSubst.ppterm_in_context subst hete
+                             CicMetaSubst.ppterm_in_context ~metasenv subst hete
                               context ^ " has type " ^
-                             CicMetaSubst.ppterm_in_context subst hety
+                             CicMetaSubst.ppterm_in_context ~metasenv subst hety
                               context ^ " but is here used with type " ^
-                             CicMetaSubst.ppterm_in_context subst s context
+                             CicMetaSubst.ppterm_in_context ~metasenv subst s context
                               (* "\nReason: " ^ Lazy.force e*))))
                     | CoercGraph.SomeCoercion candidates -> 
                         let selected = 
@@ -1476,21 +1476,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                            enrich localization_tbl hete
                             ~f:(fun _ ->
                              (lazy ("The term " ^
-                              CicMetaSubst.ppterm_in_context subst hete
+                              CicMetaSubst.ppterm_in_context ~metasenv subst hete
                                context ^ " has type " ^
-                              CicMetaSubst.ppterm_in_context subst hety
+                              CicMetaSubst.ppterm_in_context ~metasenv subst hety
                                context ^ " but is here used with type " ^
-                              CicMetaSubst.ppterm_in_context subst s context
+                              CicMetaSubst.ppterm_in_context ~metasenv subst s context
                                (* "\nReason: " ^ Lazy.force e*)))) exn))
                   | exn ->
                      enrich localization_tbl hete
                       ~f:(fun _ ->
                         (lazy ("The term " ^
-                          CicMetaSubst.ppterm_in_context subst hete
+                          CicMetaSubst.ppterm_in_context ~metasenv subst hete
                            context ^ " has type " ^
-                          CicMetaSubst.ppterm_in_context subst hety
+                          CicMetaSubst.ppterm_in_context ~metasenv subst hety
                            context ^ " but is here used with type " ^
-                          CicMetaSubst.ppterm_in_context subst s context
+                          CicMetaSubst.ppterm_in_context ~metasenv subst s context
                            (* "\nReason: " ^ Printexc.to_string exn*)))) exn
                   (* }}} end coercion stuff *)
                 in
@@ -1508,7 +1508,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
                 with RefineFailure _ | Uncertain _ as exn ->
                   (* unable to fix arity *)
-                   more_args_than_expected localization_tbl 
+                   more_args_than_expected localization_tbl metasenv
                      subst he context hetype args_bo_and_ty exn
       (* }}} *)
     in
@@ -1523,7 +1523,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
        with RefineFailure _ | Uncertain _ as exn ->
          (* unable to fix arity *)
-          more_args_than_expected localization_tbl 
+          more_args_than_expected localization_tbl metasenv
             subst he context hetype args_bo_and_ty exn
     in
     let coerced_args,subst,metasenv,he,t,ugraph =
diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index c9981bb11..86f280842 100644
--- a/components/cic_unification/cicUnification.ml
+++ b/components/cic_unification/cicUnification.ml
@@ -53,22 +53,22 @@ let foo () =
           (sprintf
            "Kernel Type checking error: 
 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
-             (CicMetaSubst.ppterm subst term)
-             (CicMetaSubst.ppterm [] term)
-             (CicMetaSubst.ppcontext subst context)
+             (CicMetaSubst.ppterm ~metasenv subst term)
+             (CicMetaSubst.ppterm ~metasenv [] term)
+             (CicMetaSubst.ppcontext ~metasenv subst context)
              (CicMetaSubst.ppmetasenv subst metasenv) 
-             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+             (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
         raise (AssertFailure msg)
     | CicTypeChecker.AssertFailure msg ->
         let msg = lazy
          (sprintf
            "Kernel Type checking assertion failure: 
 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
-             (CicMetaSubst.ppterm subst term)
-             (CicMetaSubst.ppterm [] term)
-             (CicMetaSubst.ppcontext subst context)
+             (CicMetaSubst.ppterm ~metasenv subst term)
+             (CicMetaSubst.ppterm ~metasenv [] term)
+             (CicMetaSubst.ppcontext ~metasenv subst context)
              (CicMetaSubst.ppmetasenv subst metasenv) 
-             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+             (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
         raise (AssertFailure msg)
 in profiler_toa.HExtlib.profile foo ()
 ;;
@@ -367,16 +367,16 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                     (*
                     (sprintf
                       "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
-                      (CicMetaSubst.ppterm subst t1) 
-                      (CicMetaSubst.ppterm subst t2))) *)
+                      (CicMetaSubst.ppterm ~metasenv subst t1) 
+                      (CicMetaSubst.ppterm ~metasenv subst t2))) *)
               | Invalid_argument _ ->
                   raise 
                     (UnificationFailure (lazy "2")))
                     (*
                     (sprintf
                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match." 
-                      (CicMetaSubst.ppterm subst t1) 
-                      (CicMetaSubst.ppterm subst t2)))) *)
+                      (CicMetaSubst.ppterm ~metasenv subst t1) 
+                      (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
          in subst,metasenv,ugraph1
      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
@@ -464,8 +464,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        raise (UnificationFailure (lazy 
           (sprintf
             "Can't unify %s with %s due to different constants"
-            (CicMetaSubst.ppterm subst t1) 
-            (CicMetaSubst.ppterm subst t2))))
+            (CicMetaSubst.ppterm ~metasenv subst t1) 
+            (CicMetaSubst.ppterm ~metasenv subst t2))))
    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
        if UriManager.eq uri1 uri2 && i1 = i2 then
          fo_unif_subst_exp_named_subst 
@@ -476,8 +476,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
            (lazy
             (sprintf
              "Can't unify %s with %s due to different inductive principles"
-             (CicMetaSubst.ppterm subst t1) 
-             (CicMetaSubst.ppterm subst t2))))
+             (CicMetaSubst.ppterm ~metasenv subst t1) 
+             (CicMetaSubst.ppterm ~metasenv subst t2))))
    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
@@ -489,8 +489,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
           (lazy
             (sprintf
               "Can't unify %s with %s due to different inductive constructors"
-              (CicMetaSubst.ppterm subst t1) 
-              (CicMetaSubst.ppterm subst t2))))
+              (CicMetaSubst.ppterm ~metasenv subst t1) 
+              (CicMetaSubst.ppterm ~metasenv subst t2))))
    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
                               subst context metasenv te t2 ugraph
@@ -665,7 +665,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                               subst context metasenv t1 t2' ugraph         
                         | _ -> raise 
 			    (UnificationFailure 
-			       (lazy ("not a mutind :"^CicMetaSubst.ppterm subst t2 ))))
+			       (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
                   | _ -> raise exn)))
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
@@ -685,8 +685,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
           raise (UnificationFailure (lazy "6.1")))
            (* (sprintf
               "Error trying to unify %s with %s: the number of branches is not the same." 
-              (CicMetaSubst.ppterm subst t1) 
-              (CicMetaSubst.ppterm subst t2)))) *)
+              (CicMetaSubst.ppterm ~metasenv subst t1) 
+              (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
    | (C.Rel _, _) | (_,  C.Rel _) ->
        if t1 = t2 then
          subst, metasenv,ugraph
@@ -694,8 +694,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
         raise (UnificationFailure (lazy 
            (sprintf
              "Can't unify %s with %s because they are not convertible"
-             (CicMetaSubst.ppterm subst t1) 
-             (CicMetaSubst.ppterm subst t2))))
+             (CicMetaSubst.ppterm ~metasenv subst t1) 
+             (CicMetaSubst.ppterm ~metasenv subst t2))))
    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
        let subst,metasenv,beta_expanded,ugraph1 =
          beta_expand_many 
@@ -739,8 +739,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
              raise 
                 (UnificationFailure (lazy (sprintf
                    "Can't unify %s with %s because they are not convertible"
-                   (CicMetaSubst.ppterm subst t1) 
-                   (CicMetaSubst.ppterm subst t2)))))
+                   (CicMetaSubst.ppterm ~metasenv subst t1) 
+                   (CicMetaSubst.ppterm ~metasenv subst t2)))))
 *)
    | (_,_) ->
      (* delta-beta reduction should almost never be a problem for
@@ -759,8 +759,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
         (lazy 
           (sprintf
             "Can't unify %s with %s because they are not convertible"
-            (CicMetaSubst.ppterm subst t1) 
-            (CicMetaSubst.ppterm subst t2))))
+            (CicMetaSubst.ppterm ~metasenv subst t1) 
+            (CicMetaSubst.ppterm ~metasenv subst t2))))
       else
        try
         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
@@ -771,8 +771,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
             (lazy 
               (sprintf
                 "Can't unify %s with %s because they are not convertible"
-                (CicMetaSubst.ppterm subst t1) 
-                (CicMetaSubst.ppterm subst t2))))
+                (CicMetaSubst.ppterm ~metasenv subst t1) 
+                (CicMetaSubst.ppterm ~metasenv subst t2))))
 
 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
  exp_named_subst1 exp_named_subst2 ugraph
@@ -789,7 +789,7 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
     String.concat " ; "
      (List.map
        (fun (uri,t) ->
-         UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
+         UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
        ) ens) 
    in
     raise (UnificationFailure (lazy (sprintf
@@ -809,7 +809,7 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
  lazy (
   if verbose then
    sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
-    (CicMetaSubst.ppterm subst t1)
+    (CicMetaSubst.ppterm ~metasenv subst t1)
     (try
       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
       CicPp.ppterm ty_t1
@@ -817,7 +817,7 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
     | UnificationFailure s
     | Uncertain s
     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
-    (CicMetaSubst.ppterm subst t2)
+    (CicMetaSubst.ppterm ~metasenv subst t2)
     (try
       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
       CicPp.ppterm ty_t2
@@ -825,28 +825,28 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
     | UnificationFailure s
     | Uncertain s
     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
-    (CicMetaSubst.ppcontext subst context)
+    (CicMetaSubst.ppcontext ~metasenv subst context)
     (CicMetaSubst.ppmetasenv subst metasenv)
-    (CicMetaSubst.ppsubst subst) (Lazy.force msg)
+    (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
  else
    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
-    (CicMetaSubst.ppterm_in_context subst t1 context)
+    (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
     (try
       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
-      CicMetaSubst.ppterm_in_context subst ty_t1 context
+      CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
     with 
     | UnificationFailure s
     | Uncertain s
     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
-    (CicMetaSubst.ppterm_in_context subst t2 context)
+    (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
     (try
       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
-      CicMetaSubst.ppterm_in_context subst ty_t2 context
+      CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
     with
     | UnificationFailure s
     | Uncertain s
     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
-    (CicMetaSubst.ppcontext subst context)
+    (CicMetaSubst.ppcontext ~metasenv subst context)
     (CicMetaSubst.ppmetasenv subst metasenv)
     (Lazy.force msg)
  )
diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml
index 33309f109..f06035604 100644
--- a/components/library/cicCoercion.ml
+++ b/components/library/cicCoercion.ml
@@ -216,7 +216,7 @@ let generate_composite_closure rt c1 c2 univ arity =
         let body_metasenv = order_body_menv term body_metasenv in
         debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
         let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
-        debug_print (lazy("SUBST: "^rt.RT.ppsubst subst));
+        debug_print (lazy("SUBST: "^rt.RT.ppsubst body_metasenv subst));
         let term = rt.RT.apply_subst subst term in
         debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
         (match rt.RT.type_of_aux' metasenv [] term ugraph with
diff --git a/components/library/refinementTool.ml b/components/library/refinementTool.ml
index 70af8740b..e9dae40d9 100644
--- a/components/library/refinementTool.ml
+++ b/components/library/refinementTool.ml
@@ -35,7 +35,7 @@ type kit = {
       type_of_rc;
   pack_coercion_obj: Cic.obj -> Cic.obj;
   apply_subst: Cic.substitution -> Cic.term -> Cic.term ;
-  ppsubst: Cic.substitution -> string;
+  ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string;
   ppmetasenv: Cic.substitution -> Cic.metasenv -> string;
 } 
 
diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml
index e381b3003..e7adcb7a8 100644
--- a/components/tactics/inversion.ml
+++ b/components/tactics/inversion.ml
@@ -224,7 +224,7 @@ let private_inversion_tac ~term =
   parameters_tys goalty uri_of_eq in
  (*DEBUG*)  debug_print (lazy ("cut term " ^ CicPp.ppterm cut_term));
   debug_print (lazy ("CONTEXT before apply HCUT: " ^ 
-   (CicMetaSubst.ppcontext [] context )));
+   (CicMetaSubst.ppcontext ~metasenv [] context )));
   debug_print (lazy ("termty " ^ CicPp.ppterm termty));
  (* cut DXn=DXn \to GOAL *)
  let proof1,gl1 = PET.apply_tactic (P.cut_tac cut_term) (proof,goal) in
@@ -255,7 +255,7 @@ let private_inversion_tac ~term =
  debug_print 
   (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl rightparameters))));
  debug_print (lazy ("CONTEXT before refinement: " ^ 
-  (CicMetaSubst.ppcontext [] context )));
+  (CicMetaSubst.ppcontext ~metasenv [] context )));
   (*DEBUG*) debug_print (lazy  ("private inversion: term before refinement: " ^ 
    CicPp.ppterm t));
  let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t