Fix bug #3633 properly, by delaying the interpetation of constrs in

apply f, g,... so that apply f, g. succeeds when apply f; apply g
does. It just mimicks the behavior of rewrite foo bar.

4 files changed, 94 insertions, 30 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index abaee194e..ab2dbe6ff 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -899,16 +899,12 @@ let loc_of_bindings = function
 | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
 | ExplicitBindings l -> pi1 (List.last l)
 
-let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
+let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
   let loc1 = loc_of_glob_constr c in
   let loc2 = loc_of_bindings bl in
   let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in
-  let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
-  sigma, (loc,cb)
-
-let interp_open_constr_with_bindings_arg_loc ist env sigma (keep,c) =
-  let sigma, c = interp_open_constr_with_bindings_loc ist env sigma c in
-  sigma,(keep,c)
+  let f env sigma = interp_open_constr_with_bindings ist env sigma cb in
+    (loc,f)
 
 let interp_induction_arg ist gl arg =
   let env = pf_env gl and sigma = project gl in
@@ -1704,14 +1700,15 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-        let sigma, l =
-          List.fold_map (interp_open_constr_with_bindings_arg_loc ist env) sigma cb
-        in
+	let l = List.map (fun (k,c) ->
+          let loc, f = interp_open_constr_with_bindings_loc ist c in
+	    (k,(loc,f))) cb 
+	in
         let sigma,tac = match cl with
-          | None -> sigma, fun l -> Tactics.apply_with_bindings_gen a ev l
+          | None -> sigma, fun l -> Tactics.apply_with_delayed_bindings_gen a ev l
           | Some cl ->
               let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in
-              sigma, fun l -> Tactics.apply_in a ev clear id l cl in
+              sigma, fun l -> Tactics.apply_delayed_in a ev clear id l cl in
         Tacticals.New.tclWITHHOLES ev tac sigma l
       end
   | TacElim (ev,(keep,cb),cbo) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 36a297c81..a495c8783 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -574,8 +574,10 @@ let find_intro_names ctxt gl =
 
 let build_intro_tac id dest tac = match dest with
   | MoveLast -> Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id)
-  | dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
-
+  | dest -> Tacticals.New.tclTHENLIST 
+    [Proofview.V82.tactic (introduction id); 
+     Proofview.V82.tactic (move_hyp true id dest); tac id]
+    
 let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
@@ -600,7 +602,8 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
 	     (intro_then_gen name_flag move_flag false dep_flag tac))
           begin function
             | RefinerError IntroNeedsProduct ->
-                Proofview.tclZERO (Errors.UserError("Intro",str "No product even after head-reduction."))
+                Proofview.tclZERO 
+		  (Errors.UserError("Intro",str "No product even after head-reduction."))
             | e -> Proofview.tclZERO e
           end
   end
@@ -676,7 +679,9 @@ let intros_possibly_replacing ids =
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     let posl = List.map (fun id -> (id,get_next_hyp_position id hyps)) ids in
     Tacticals.New.tclTHEN
-      (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id]))) (if suboptimal then ids else List.rev ids))
+      (Tacticals.New.tclMAP (fun id -> 
+	Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id])))
+	 (if suboptimal then ids else List.rev ids))
       (Tacticals.New.tclMAP (fun (id,pos) ->
         Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id))
          posl)
@@ -856,11 +861,13 @@ let do_replace id = function
    [Ti] and the first one (resp last one) being [G] whose hypothesis
    [id] is replaced by P using the proof given by [tac] *)
 
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) targetid id sigma0 clenv tac =
+let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) 
+    targetid id sigma0 clenv tac =
   let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in
   let clenv =
     if with_classes then
-      { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd }
+      { clenv with evd = Typeclasses.resolve_typeclasses 
+	  ~fail:(not with_evars) clenv.env clenv.evd }
     else clenv
   in
   let new_hyp_typ = clenv_type clenv in
@@ -945,7 +952,8 @@ let enforce_prop_bound_names rename tac =
   | _ ->
       tac
 
-let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause =
+let elimination_clause_scheme with_evars ?(flags=elim_flags ()) 
+    rename i (elim, elimty, bindings) indclause =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -1097,7 +1105,8 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
     (* Set the hypothesis name in the message *)
     raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
 
-let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause =
+let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) 
+    id rename i (elim, elimty, bindings) indclause =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -1202,11 +1211,12 @@ let descend_in_conjunctions avoid tac exit c =
 	    match make_projection env sigma params cstr sign elim i n c u with
 	    | None -> Tacticals.New.tclFAIL 0 (mt())
 	    | Some (p,pt) ->
-	    Tacticals.New.tclTHENS
-	      (assert_before_gen false (NamingAvoid avoid) pt)
-	      [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *)
-	       Tacticals.New.onLastHypId (tac (not isrec))]
-            end))
+	      Tacticals.New.tclTHENS
+		(assert_before_gen false (NamingAvoid avoid) pt)
+		[Proofview.V82.tactic (refine p);
+		 (* Might be ill-typed due to forbidden elimination. *)
+		 Tacticals.New.onLastHypId (tac (not isrec))]
+           end))
     | None ->
 	raise Exit
   with RefinerError _|UserError _|Exit -> exit ()
@@ -1312,6 +1322,24 @@ let rec apply_with_bindings_gen b e = function
         (general_apply b b e k cb)
         (apply_with_bindings_gen b e cbl)
 
+let apply_with_delayed_bindings_gen b e l = 
+  let one k (loc, f) =
+    Proofview.Goal.enter begin fun gl ->
+      let sigma = Proofview.Goal.sigma gl in
+      let env = Proofview.Goal.env gl in
+      let sigma, cb = f env sigma in
+	Tacticals.New.tclWITHHOLES e
+          (general_apply b b e k) sigma (loc,cb)
+    end
+  in
+  let rec aux = function
+    | [] -> Proofview.tclUNIT ()
+    | [k,f] -> one k f
+    | (k,f)::cbl ->
+      Tacticals.New.tclTHENLAST
+        (one k f) (aux cbl)
+  in aux l
+
 let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)]
 
 let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(dloc,cb)]
@@ -1396,6 +1424,17 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
   aux [] with_destruct d
   end
 
+let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming
+    id (clear_flag,(loc,f)) tac =
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let sigma, c = f env sigma in
+      Proofview.V82.tclEVARS sigma <*>
+	(apply_in_once sidecond_first with_delta with_destruct with_evars naming id 
+	   (clear_flag,(loc,c)) tac)
+  end
+
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
 
@@ -1670,7 +1709,9 @@ let constructor_tac with_evars expctdnumopt i lbind =
 	
       let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in
 	(Tacticals.New.tclTHENLIST
-           [Proofview.V82.tclEVARS sigma; Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
+           [Proofview.V82.tclEVARS sigma; 
+	    Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); 
+	    intros; apply_tac])
   end
 
 let one_constructor i lbind = constructor_tac false None i lbind
@@ -1799,7 +1840,8 @@ let rewrite_hyp assert_style l2r id =
     | Some (hdcncl,[c]) ->
         let l2r = not l2r in (* equality of the form eq_true *)
         if isVar c then
-          Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c))
+          Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) 
+	    (Proofview.V82.tactic (clear_var_and_eq c))
         else
           Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
     | _ ->
@@ -1988,7 +2030,7 @@ let assert_as first ipat c =
 let general_apply_in sidecond_first with_delta with_destruct with_evars
     with_clear id lemmas ipat =
   let tac (naming,lemma) tac id =
-    apply_in_once sidecond_first with_delta with_destruct with_evars
+    apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
       naming id lemma tac in
   let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in
   let lemmas_target, last_lemma_target =
@@ -2007,6 +2049,10 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
 *)
 
 let apply_in simple with_evars clear_flag id lemmas ipat =
+  let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, fun _ sigma -> sigma, l)) lemmas in
+  general_apply_in false simple simple with_evars clear_flag id lemmas ipat
+
+let apply_delayed_in simple with_evars clear_flag id lemmas ipat =
   general_apply_in false simple simple with_evars clear_flag id lemmas ipat
 
 (*****************************)
@@ -2085,7 +2131,8 @@ let forward b usetac ipat c =
   | None ->
       Proofview.Goal.enter begin fun gl ->
       let t = Tacmach.New.pf_type_of gl  c in
-      Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
+      Tacticals.New.tclTHENFIRST (assert_as true ipat t)
+	(Proofview.V82.tactic (exact_no_check c))
       end
   | Some tac ->
       if b then
@@ -2336,7 +2383,9 @@ let check_unused_names names =
   if not (List.is_empty names) && Flags.is_verbose () then
     msg_warning
       (str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
-       ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (snd (c (Global.env()) Evd.empty)))) names)
+       ++ str": " ++ prlist_with_sep spc 
+	 (Miscprint.pr_intro_pattern 
+	    (fun c -> Printer.pr_constr (snd (c (Global.env()) Evd.empty)))) names)
 
 let intropattern_of_name gl avoid = function
   | Anonymous -> IntroNaming IntroAnonymous
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c076efb1f..398a90ba3 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -188,6 +188,9 @@ val eapply                : constr -> unit Proofview.tactic
 val apply_with_bindings_gen :
   advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> unit Proofview.tactic
 
+val apply_with_delayed_bindings_gen :
+  advanced_flag -> evars_flag -> (clear_flag * delayed_open_constr_with_bindings located) list -> unit Proofview.tactic
+
 val apply_with_bindings   : constr with_bindings -> unit Proofview.tactic
 val eapply_with_bindings  : constr with_bindings -> unit Proofview.tactic
 
@@ -198,6 +201,11 @@ val apply_in :
     (clear_flag * constr with_bindings located) list ->
     intro_pattern option -> unit Proofview.tactic
 
+val apply_delayed_in :
+  advanced_flag -> evars_flag -> clear_flag -> Id.t -> 
+    (clear_flag * delayed_open_constr_with_bindings located) list ->
+    intro_pattern option -> unit Proofview.tactic
+
 (** {6 Elimination tactics. } *)
 
 (*
diff --git a/test-suite/bugs/closed/3633.v b/test-suite/bugs/closed/3633.v
new file mode 100644
index 000000000..6a952377c
--- /dev/null
+++ b/test-suite/bugs/closed/3633.v
@@ -0,0 +1,10 @@
+Set Typeclasses Strict Resolution.
+Class Contr (A : Type) := { center : A }.
+Definition foo {A} `{Contr A} : A.
+Proof.
+  apply center.
+  Undo.
+  (* Ensure the constraints are solved independently, otherwise a frozen ?A 
+  makes a search for Contr ?A fail when finishing to apply (fun x => x) *)
+  apply (fun x => x), center. 
+Qed.
\ No newline at end of file