From 852e6f960d3fc6d4cf702ab21cfe813d9edbb531 Mon Sep 17 00:00:00 2001
From: Armaël Guéneau <armael.gueneau@ens-lyon.fr>
Date: Thu, 31 May 2018 14:17:39 +0200
Subject: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-

---
 plugins/ltac/extratactics.ml4 | 71 -------------------------------------------
 1 file changed, 71 deletions(-)

(limited to 'plugins/ltac')

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
@@ -284,77 +284,6 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint
   [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ]
 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                                                             *)
 
-- 
cgit v1.2.3