summaryrefslogtreecommitdiff
path: root/print.ml
diff options
context:
space:
mode:
authorGravatar Nicolas Braud-Santoni <nicolas@braud-santoni.eu>2016-07-23 16:21:44 -0400
committerGravatar Nicolas Braud-Santoni <nicolas@braud-santoni.eu>2016-07-23 16:21:44 -0400
commit17564e4922acda6b72bf39de7a8c23ed0c0178f6 (patch)
tree9551ca9435f64c019dbef48894f5dd0c64045f1c /print.ml
parenta77bca84565b26aeedec3b210d761240d9d261f4 (diff)
Imported Upstream version 8.5.1
Diffstat (limited to 'print.ml')
-rw-r--r--print.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/print.ml b/print.ml
index 1ceb786..0305158 100644
--- a/print.ml
+++ b/print.ml
@@ -65,7 +65,7 @@ let pp_all pt : (int * Terms.t * named_env Search_monad.m) Search_monad.m -> Pp.
rename the variables, and rebuilds raw Coq terms (for the context, and
the terms in the environment). In order to do so, it requires the
information gathered by the {!Theory.Trans} module.*)
-let print rlt ir m (context : Term.rel_context) goal =
+let print rlt ir m (context : Context.rel_context) goal =
if Search_monad.count m = 0
then
(
@@ -80,7 +80,7 @@ let print rlt ir m (context : Term.rel_context) goal =
let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in
let l =
List.map (fun (v,t) ->
- let (name,body,types) = Term.lookup_rel v context in
+ let (name,body,types) = Context.lookup_rel v context in
(name,t)
) l
in