From 856780b163fdcd5e36a1d4af99034e3af6fde1d7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 2 Apr 2016 21:24:46 +0200
Subject: Fixing the "No applicable tactic" non informative error message
 regression on apply.

---
 tactics/tactics.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f23808f6f9..28aed8a10e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1429,7 +1429,8 @@ let descend_in_conjunctions avoid tac (err, info) c =
 	  with Not_found ->
 	    let elim = build_case_analysis_scheme env sigma (ind,u) false sort in
 	    NotADefinedRecordUseScheme (snd elim) in
-	Tacticals.New.tclFIRST
+	Tacticals.New.tclORELSE0
+	(Tacticals.New.tclFIRST
 	  (List.init n (fun i ->
             Proofview.Goal.enter begin fun gl ->
             let env = Proofview.Goal.env gl in
@@ -1442,7 +1443,8 @@ let descend_in_conjunctions avoid tac (err, info) c =
 		[Proofview.V82.tactic (refine p);
 		 (* Might be ill-typed due to forbidden elimination. *)
 		 Tacticals.New.onLastHypId (tac (not isrec))]
-           end))
+           end)))
+          (Proofview.tclZERO ~info err)
     | None -> Proofview.tclZERO ~info err
   with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
   end
-- 
cgit v1.2.3


From 83608720aac2a0a464649aca8b2a23ce395679ae Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 7 Apr 2016 14:58:27 +0200
Subject: Fixing an incorrect use of prod_appvect on a term which was not a
 product in setoid_rewrite.

Backport of d670c6b6ce from trunk.
---
 tactics/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 803e187ff5..21abafbf18 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1028,7 +1028,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		      | x -> x
 		    in
 		    let res =
-		      { rew_car = prod_appvect r.rew_car args;
+		      { rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args;
 			rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
 			rew_prf = prf; rew_evars = r.rew_evars }
 		    in 
-- 
cgit v1.2.3


From 9f0a896536e709880de5ba638069dea680803f62 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 7 Apr 2016 15:50:26 +0200
Subject: Allow to unset the refinement mode of Instance in ML

Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
---
 tactics/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 21abafbf18..9d70c177b4 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1725,7 +1725,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 let anew_instance global binders instance fields =
   new_instance (Flags.is_universe_polymorphism ()) 
     binders instance (Some (true, CRecord (Loc.ghost,None,fields)))
-    ~global ~generalize:false None
+    ~global ~generalize:false ~refine:false None
 
 let declare_instance_refl global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
-- 
cgit v1.2.3