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

2 files changed, 33 insertions, 0 deletions

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