aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index d573a9f053..3aab39eda1 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1403,7 +1403,7 @@ let print_env_short env =
| RelDecl.LocalAssum (n,_) -> pr_name n
| RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
in
- let pr_named_decl = pr_rel_decl % NamedDecl.to_rel in
+ let pr_named_decl = pr_rel_decl % NamedDecl.to_rel_decl in
let nc = List.rev (named_context env) in
let rc = List.rev (rel_context env) in
str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++