diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_minicoq.ml4 | 4 | ||||
| -rw-r--r-- | parsing/g_minicoq.mli | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 index c14c5d0344..21163804ec 100644 --- a/parsing/g_minicoq.ml4 +++ b/parsing/g_minicoq.ml4 @@ -7,7 +7,7 @@ open Names open Univ open Generic open Term -open Sign +open Environ let lexer = { Token.func = Lexer.func; @@ -176,5 +176,5 @@ let rec pp bv = function | Rel n -> print_rel bv n | _ -> [< 'sTR"<???>" >] -let pr_term _ ctx = pp (it_dbenv (fun l n _ -> n::l) [] ctx) +let pr_term _ ctx = pp (fold_rel_context (fun _ (n,_,_) l -> n::l) ctx []) diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli index de3a022862..db5c0d07f5 100644 --- a/parsing/g_minicoq.mli +++ b/parsing/g_minicoq.mli @@ -3,7 +3,7 @@ open Pp open Names open Term -open Sign +open Environ (*i*) val term : constr Grammar.Entry.e @@ -19,4 +19,4 @@ type command = val command : command Grammar.Entry.e -val pr_term : path_kind -> context -> constr -> std_ppcmds +val pr_term : path_kind -> env -> constr -> std_ppcmds |