ppcontext (and thus also ppmetasenv) were buggy: the occurrences of a variable

bound to a previous entry were of the form -n (instead of showing the binder)

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index acb942ec5f37b9c4000a7b72c57e79a424b457eb..30069cdfec88d12f6549922d14d0c1a6561adf90 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -64,7 +64,6 @@ let rec force_does_not_occur subst to_be_restricted t =
                  try
                    Some (aux k t)
                  with Occur ->
-prerr_endline (Printf.sprintf "RESTRINGO (%d,%d)" n !i) ;
                    more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
                    None)
            l
@@ -477,25 +476,36 @@ let apply_subst_metasenv subst metasenv =
 
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
-let ppcontext ?(sep = "\n") subst context =
-  String.concat sep
-    (List.rev_map (function
-      | Some (n, Cic.Decl t) ->
-          sprintf "%s : %s" (CicPp.ppname n) (ppterm subst t)
-      | Some (n, Cic.Def (t, ty)) ->
-          sprintf "%s : %s := %s"
-            (CicPp.ppname n)
-            (match ty with None -> "_" | Some ty -> ppterm subst ty)
-            (ppterm subst t)
-      | None -> "_")
-      context)
+let ppterm_in_context subst term name_context =
+ CicPp.pp (apply_subst subst term) name_context
+
+let ppcontext' ?(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_context 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_context subst ty name_context)
+          (ppterm_in_context subst bo name_context), (Some n)::name_context
+       | None ->
+          sprintf "%s_ :? _" (separate i), None::name_context
+    ) context ("",[])
+
+let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
 
 let ppmetasenv ?(sep = "\n") metasenv subst =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
-        sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i
-          (ppterm subst t))
+        let context,name_context = ppcontext' ~sep:"; " subst c in
+         sprintf "%s |- ?%d: %s" context i
+          (ppterm_in_context subst t name_context))
       (List.filter
         (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
         metasenv))