diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 4 | ||||
| -rw-r--r-- | tactics/autorewrite.mli | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 6 |
3 files changed, 7 insertions, 5 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 51708670f5..4b1b473b33 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -75,7 +75,9 @@ let find_matches bas pat = let res = HintDN.search_pattern base pat in List.map snd res -let print_rewrite_hintdb env sigma bas = +let print_rewrite_hintdb bas = + let env = Global.env () in + let sigma = Evd.from_env env in (str "Database " ++ str bas ++ fnl () ++ prlist_with_sep fnl (fun h -> diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 03e9414e0f..4c6146d745 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -42,7 +42,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic -val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t +val print_rewrite_hintdb : string -> Pp.t open Clenv diff --git a/tactics/equality.ml b/tactics/equality.ml index 45a4799ea1..51eee2a053 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -735,7 +735,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = let project env sorts posn t1 t2 = let ty1 = get_type_of env sigma t1 in let s = get_sort_family_of ~truncation_style:true env sigma ty1 in - if Sorts.List.mem s sorts + if List.mem_f Sorts.family_equal s sorts then [(List.rev posn,t1,t2)] else [] in let rec findrec sorts posn t1 t2 = @@ -746,7 +746,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = when Int.equal (List.length args1) (constructor_nallargs env sp1) -> let sorts' = - Sorts.List.intersect sorts (allowed_sorts env (fst sp1)) + CList.intersect Sorts.family_equal sorts (sorts_below (top_allowed_sort env (fst sp1))) in (* both sides are fully applied constructors, so either we descend, or we can discriminate here. *) @@ -762,7 +762,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = List.flatten (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn)) 0 rargs1 rargs2) - else if Sorts.List.mem InType sorts' && not no_discr + else if List.mem_f Sorts.family_equal InType sorts' && not no_discr then (* see build_discriminator *) raise (DiscrFound (List.rev posn,sp1,sp2)) else |