diff options
Diffstat (limited to 'print.ml')
| -rw-r--r-- | print.ml | 11 |
1 files changed, 6 insertions, 5 deletions
@@ -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 ) |