Merge branch 'v8.5' into trunk

2 files changed, 39 insertions, 14 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 2ee9a6c98..be47293fc 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -337,11 +337,18 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
+let constr_flags = {
+  Pretyping.use_typeclasses = true;
+  Pretyping.use_unif_heuristics = true;
+  Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+  Pretyping.fail_evar = false;
+  Pretyping.expand_evars = true }
+
 let refine_tac ist simple c =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let flags = Pretyping.all_no_fail_flags in
+    let flags = constr_flags in
     let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
@@ -517,11 +524,29 @@ VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF
     [ add_transitivity_lemma false t ]
 END
 
+let cache_implicit_tactic (_,tac) = match tac with
+  | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac)
+  | None -> Pfedit.clear_implicit_tactic ()
+
+let subst_implicit_tactic (subst,tac) =
+  Option.map (Tacsubst.subst_tactic subst) tac
+
+let inImplicitTactic : glob_tactic_expr option -> obj =
+  declare_object {(default_object "IMPLICIT-TACTIC") with
+       open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o);
+       cache_function = cache_implicit_tactic;
+       subst_function = subst_implicit_tactic;
+       classify_function = (fun o -> Dispose)}
+
+let declare_implicit_tactic tac =
+  Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac)))
+
+let clear_implicit_tactic () =
+  Lib.add_anonymous_leaf (inImplicitTactic None)
+
 VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF
-| [ "Declare" "Implicit" "Tactic" tactic(tac) ] ->
-    [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ]
-| [ "Clear" "Implicit" "Tactic" ] ->
-    [ Pfedit.clear_implicit_tactic () ]
+| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ]
+| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ]
 END
 
 
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 00722ac28..455b871c8 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -424,7 +424,7 @@ let intern_hyp_location ist ((occs,id),hl) =
 (* Reads a pattern *)
 let intern_pattern ist ?(as_type=false) ltacvars = function
   | Subterm (b,ido,pc) ->
-      let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in
+      let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
       ido, metas, Subterm (b,ido,pc)
   | Term pc ->
       let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
@@ -446,7 +446,7 @@ let opt_cons accu = function
 | Some id -> Id.Set.add id accu
 
 (* Reads the hypotheses of a "match goal" rule *)
-let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
+let rec intern_match_goal_hyps ist lfun = function
   | (Hyp ((_,na) as locna,mp))::tl ->
       let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
       let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
@@ -455,7 +455,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
   | (Def ((_,na) as locna,mv,mp))::tl ->
       let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
       let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
-      let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in
+      let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
       let lfun' = name_cons (opt_cons (opt_cons lfun ido) ido') na in
       lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
   | [] -> lfun, [], []
@@ -564,7 +564,7 @@ and intern_tactic_seq onlytac ist = function
       ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
 
   | TacMatchGoal (lz,lr,lmr) ->
-      ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist ~as_type:true lmr))
+      ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr)
   | TacMatch (lz,c,lmr) ->
       ist.ltacvars,
       TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
@@ -668,18 +668,18 @@ and intern_tacarg strict onlytac ist = function
     TacGeneric arg
 
 (* Reads the rules of a Match Context or a Match *)
-and intern_match_rule onlytac ist ?(as_type=false) = function
+and intern_match_rule onlytac ist = function
   | (All tc)::tl ->
-      All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist ~as_type tl)
+      All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
   | (Pat (rl,mp,tc))::tl ->
       let {ltacvars=lfun; genv=env} = ist in
-      let lfun',metas1,hyps = intern_match_goal_hyps ist ~as_type lfun rl in
-      let ido,metas2,pat = intern_pattern ist ~as_type lfun mp in
+      let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
+      let ido,metas2,pat = intern_pattern ist lfun mp in
       let fold accu x = Id.Set.add x accu in
       let ltacvars = List.fold_left fold (opt_cons lfun' ido) metas1 in
       let ltacvars = List.fold_left fold ltacvars metas2 in
       let ist' = { ist with ltacvars } in
-      Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist ~as_type tl)
+      Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
   | [] -> []
 
 and intern_genarg ist (GenArg (Rawwit wit, x)) =