aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_minicoq.ml43
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index bf75cdd381..c14c5d0344 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -176,4 +176,5 @@ let rec pp bv = function
| Rel n -> print_rel bv n
| _ -> [< 'sTR"<???>" >]
-let pr_term _ ctx = pp (List.map fst (get_rels ctx))
+let pr_term _ ctx = pp (it_dbenv (fun l n _ -> n::l) [] ctx)
+