From 17564e4922acda6b72bf39de7a8c23ed0c0178f6 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Sat, 23 Jul 2016 16:21:44 -0400 Subject: Imported Upstream version 8.5.1 --- print.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'print.ml') 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 -- cgit v1.2.3