diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 7 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 4 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.ml4 | 2 |
3 files changed, 3 insertions, 10 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index c01214377c..76db2f3c2f 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -25,7 +25,7 @@ let init_size=5 let cc_verbose=ref false let debug x = - if !cc_verbose then msg_debug (x ()) + if !cc_verbose then Feedback.msg_debug (x ()) let _= let gdopt= @@ -154,11 +154,6 @@ let rec term_equal t1 t2 = open Hashset.Combine -let hash_sorts_family = function -| InProp -> 0 -| InSet -> 1 -| InType -> 2 - let rec hash_term = function | Symb c -> combine 1 (hash_constr c) | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c8924073c7..bd788a425a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -424,10 +424,10 @@ let cc_tactic depth additionnal_terms = List.map (build_term_to_complete uf newmeta) (epsilons uf) in - Pp.msg_info + Feedback.msg_info (Pp.str "Goal is solvable by congruence but \ some arguments are missing."); - Pp.msg_info + Feedback.msg_info (Pp.str " Try " ++ hov 8 begin diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 9a53e2e16a..52a1351199 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -11,8 +11,6 @@ open Cctac open Stdarg open Constrarg -open Pcoq.Prim -open Pcoq.Constr DECLARE PLUGIN "cc_plugin" |