From 1117d2e4a00debfbfa0157cc3e780916df72c26b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:06:42 +0000 Subject: New upstream version 8.6 --- print.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'print.ml') diff --git a/print.ml b/print.ml index 0305158..427b6dc 100644 --- a/print.ml +++ b/print.ml @@ -10,6 +10,8 @@ solution *) open Pp open Matcher +open Context.Rel.Declaration + type named_env = (Names.name * Terms.t) list @@ -65,14 +67,14 @@ 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 : Context.rel_context) goal = +let print rlt ir m (context : Context.Rel.t) goal = if Search_monad.count m = 0 then ( Tacticals.tclFAIL 0 (Pp.str "No subterm modulo AC") goal ) else - let _ = Pp.msgnl (Pp.str "All solutions:") in + let _ = Feedback.msg_notice (Pp.str "All solutions:") in let m = Search_monad.(>>) m (fun (i,t,envm) -> let envm = Search_monad.(>>) envm ( fun env -> @@ -80,8 +82,7 @@ let print rlt ir m (context : Context.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) = Context.lookup_rel v context in - (name,t) + get_name (Context.Rel.lookup v context), t ) l in Search_monad.return l @@ -91,7 +92,7 @@ let print rlt ir m (context : Context.rel_context) goal = ) in let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in - let _ = Pp.msgnl + let _ = Feedback.msg_notice (pp_all (fun t -> Printer.pr_constr (Theory.Trans.raw_constr_of_t ir rlt context t) ) m ) -- cgit v1.2.3