From 6c4eceaa9d71df6cb608b056bebbd760b707d26e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 12:50:26 +0200
Subject: Factorize hint flags in Class_tatcis.make_make_resolve_hyp.

They were always instantiated with the triple (true, false, false).
---
 tactics/class_tactics.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics/class_tactics.ml')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 195073d7aa..72234db688 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -499,7 +499,7 @@ let evars_to_goals p evm =
   else Some (goals, nongoals)
 
 (** Making local hints  *)
-let make_resolve_hyp env sigma st flags only_classes pri decl =
+let make_resolve_hyp env sigma st only_classes pri decl =
   let id = NamedDecl.get_id decl in
   let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in
   let rec iscl env ty =
@@ -530,7 +530,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
                hints)
         else []
       in
-        (hints @ make_resolves env sigma flags pri ~name ~check:false ~poly:false (IsGlobRef id))
+        (hints @ make_resolves env sigma (true, false, false) pri ~name ~check:false ~poly:false (IsGlobRef id))
     else []
 
 let make_hints g (modes,st) only_classes sign =
@@ -546,7 +546,7 @@ let make_hints g (modes,st) only_classes sign =
         in
         if consider then
           let hint =
-            pf_apply make_resolve_hyp g st (true,false,false) only_classes empty_hint_info hyp
+            pf_apply make_resolve_hyp g st only_classes empty_hint_info hyp
           in hint @ hints
         else hints)
       ([]) sign
@@ -793,7 +793,7 @@ module Search = struct
     let decl = Tacmach.New.pf_last_hyp gl in
     let hint =
       make_resolve_hyp env sigma (Hint_db.transparent_state info.search_hints)
-                       (true,false,false) info.search_only_classes empty_hint_info decl in
+                       info.search_only_classes empty_hint_info decl in
     let ldb = Hint_db.add_list env sigma hint info.search_hints in
     let info' =
       { info with search_hints = ldb; last_tac = lazy (str"intro");
-- 
cgit v1.2.3