diff options
| author | filliatr | 2000-07-25 17:29:20 +0000 |
|---|---|---|
| committer | filliatr | 2000-07-25 17:29:20 +0000 |
| commit | c330f60f1617afcb42cebe2fd2ccf9f330ea4f89 (patch) | |
| tree | 53e61f40e19ea35216091af7324a6bbd4fc7e4bd /parsing | |
| parent | 968d65c616127446c5f1c5d3485e9efdc420e6a4 (diff) | |
retablissement make doc et make minicoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@571 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |