Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-

6 files changed, 42 insertions, 79 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index c5254b37c..8813c7764 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -285,77 +285,6 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint
 END
 
 (**********************************************************************)
-(* Hint Resolve                                                       *)
-
-open EConstr
-open Vars
-open Coqlib
-
-let project_hint ~poly pri l2r r =
-  let gr = Smartlocate.global_with_alias r in
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
-  let sigma, c = Evd.fresh_global env sigma gr in
-  let t = Retyping.get_type_of env sigma c in
-  let t =
-    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
-  let sign,ccl = decompose_prod_assum sigma t in
-  let (a,b) = match snd (decompose_app sigma ccl) with
-    | [a;b] -> (a,b)
-    | _ -> assert false in
-  let p =
-    if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let sigma, p = Evd.fresh_global env sigma p in
-  let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
-  let c = it_mkLambda_or_LetIn
-    (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
-  let id =
-    Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
-  in
-  let ctx = Evd.const_univ_entry ~poly sigma in
-  let c = EConstr.to_constr sigma c in
-  let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
-  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-    (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
-
-let add_hints_iff ~atts l2r lc n bl =
-  let open Vernacinterp in
-  Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl
-    (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
-
-VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
-  [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
-    ":" preident_list(bl) ] ->
-  [ fun ~atts ~st -> begin
-        add_hints_iff ~atts true lc n bl;
-        st
-      end
-  ]
-| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
-  [ fun ~atts ~st -> begin
-        add_hints_iff ~atts true lc n ["core"];
-        st
-      end
-  ]
-END
-
-VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
-  [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
-    ":" preident_list(bl) ] ->
-  [ fun ~atts ~st -> begin
-        add_hints_iff ~atts false lc n bl;
-        st
-      end
-  ]
-| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
-  [ fun ~atts ~st -> begin
-        add_hints_iff ~atts false lc n ["core"];
-        st
-      end
-  ]
-END
-
-(**********************************************************************)
 (* Refine                                                             *)
 
 open EConstr
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4b77418ff..d49c8aaa5 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -167,6 +167,7 @@ type hint_mode =
 
 type hints_expr =
   | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+  | HintsResolveIFF of bool * reference list * int option
   | HintsImmediate of reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
@@ -1290,6 +1291,35 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     else (Lib.add_anonymous_leaf (input_context_set diff);
 	  IsConstr (c', Univ.ContextSet.empty))
 
+let project_hint ~poly pri l2r r =
+  let open EConstr in
+  let open Coqlib in
+  let gr = Smartlocate.global_with_alias r in
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  let sigma, c = Evd.fresh_global env sigma gr in
+  let t = Retyping.get_type_of env sigma c in
+  let t =
+    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
+  let sign,ccl = decompose_prod_assum sigma t in
+  let (a,b) = match snd (decompose_app sigma ccl) with
+    | [a;b] -> (a,b)
+    | _ -> assert false in
+  let p =
+    if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
+  let sigma, p = Evd.fresh_global env sigma p in
+  let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
+  let c = it_mkLambda_or_LetIn
+    (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
+  let id =
+    Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
+  in
+  let ctx = Evd.const_univ_entry ~poly sigma in
+  let c = EConstr.to_constr sigma c in
+  let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
+  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
+    (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
+
 let interp_hints poly =
   fun h ->
   let env = Global.env () in
@@ -1319,6 +1349,8 @@ let interp_hints poly =
   in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
+  | HintsResolveIFF (l2r, lc, n) ->
+    HintsResolveEntry (List.map (project_hint ~poly n l2r) lc)
   | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
   | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
   | HintsTransparency (lhints, b) ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 7ef7f0185..e958f986e 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -83,6 +83,7 @@ type hint_mode =
 
 type hints_expr =
   | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+  | HintsResolveIFF of bool * Libnames.reference list * int option
   | HintsImmediate of reference_or_constr list
   | HintsUnfold of Libnames.reference list
   | HintsTransparency of Libnames.reference list * bool
diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4
index 56229c765..a3806ff68 100644
--- a/vernac/g_proofs.ml4
+++ b/vernac/g_proofs.ml4
@@ -98,15 +98,8 @@ GEXTEND Gram
 	    VernacCreateHintDb (id, b)
       | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
 	  VernacRemoveHints (dbnames, ids)
-      | IDENT "Hint"; h = hint;
-	  dbnames = opt_hintbases ->
+      | IDENT "Hint"; h = hint; dbnames = opt_hintbases ->
           VernacHints (dbnames, h)
-      (* Declare "Resolve" explicitly so as to be able to later extend with
-         "Resolve ->" and "Resolve <-" *)
-      | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; 
-	info = hint_info; dbnames = opt_hintbases ->
-          VernacHints (dbnames,
-	    HintsResolve (List.map (fun x -> (info, true, x)) lc))
       ] ];
   reference_or_constr:
    [ [ r = global -> HintsReference r
@@ -115,6 +108,10 @@ GEXTEND Gram
   hint:
     [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info ->
           HintsResolve (List.map (fun x -> (info, true, x)) lc)
+      | IDENT "Resolve"; "->"; lc = LIST1 global; n = OPT natural ->
+          HintsResolveIFF (true, lc, n)
+      | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural ->
+          HintsResolveIFF (false, lc, n)
       | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc
       | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
       | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 7aff758e9..5490b9ce5 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -200,6 +200,9 @@ open Pputils
           keyword "Resolve " ++ prlist_with_sep sep
             (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info)
             l
+        | HintsResolveIFF (l2r, l, n) ->
+          keyword "Resolve " ++ str (if l2r then "->" else "<-")
+          ++ prlist_with_sep sep pr_reference l
         | HintsImmediate l ->
           keyword "Immediate" ++ spc() ++
             prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index fb40f0d9c..9e8dfc4f8 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -124,6 +124,7 @@ type hint_info_expr = Hints.hint_info_expr
 
 type hints_expr = Hints.hints_expr =
   | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
+  | HintsResolveIFF of bool * reference list * int option
   | HintsImmediate of Hints.reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool