diff options
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index ed612c0fc9..de98f63823 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -9,7 +9,7 @@ open Equality open Names open Pp -open Term +open Constr open Termops open CErrors open Util @@ -20,7 +20,7 @@ open Locus type rew_rule = { rew_lemma: constr; rew_type: types; rew_pat: constr; - rew_ctx: Univ.universe_context_set; + rew_ctx: Univ.ContextSet.t; rew_l2r: bool; rew_tac: Genarg.glob_generic_argument option } @@ -73,12 +73,12 @@ let find_matches bas pat = let res = HintDN.search_pattern base pat in List.map snd res -let print_rewrite_hintdb bas = +let print_rewrite_hintdb env sigma bas = (str "Database " ++ str bas ++ fnl () ++ prlist_with_sep fnl (fun h -> str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ - Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ + Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++ Option.cata (fun tac -> str " then use tactic " ++ Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) |