diff options
Diffstat (limited to 'plugins/ltac/extratactics.ml4')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 2e90ce90c..797dfbe23 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -296,7 +296,6 @@ let project_hint ~poly pri l2r r = let env = Global.env() in let sigma = Evd.from_env env in let sigma, c = Evd.fresh_global env sigma gr in - let c = EConstr.of_constr c 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 @@ -307,7 +306,6 @@ let project_hint ~poly pri l2r r = 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 p = EConstr.of_constr 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 @@ -317,7 +315,7 @@ let project_hint ~poly pri l2r r = 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 = {Vernacexpr.hint_priority = pri; hint_pattern = None} 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 = |