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(-)

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 59cb5ca9b6c0e29fe65e9ae99dfd6cabafc52be6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 28 Oct 2015 15:17:30 -0400
Subject: Add compatibility Nonrecursive Elimination Schemes

---
 theories/Compat/Coq84.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 90083b00d9..d695ef1d89 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -15,6 +15,9 @@ Ltac omega := Coq.omega.Omega.omega.
 (** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *)
 Global Set Asymmetric Patterns.
 
+(** The automatic elimination schemes for records were dropped by default in 8.5.  This restores the default behavior of Coq 8.4. *)
+Global Set Nonrecursive Elimination Schemes.
+
 (** See bug 3545 *)
 Global Set Universal Lemma Under Conjunction.
 
-- 
cgit v1.2.3


From 4c078b0362542908eb2fe1d63f0d867b339953fd Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 29 Dec 2015 13:21:17 -0500
Subject: Update Coq84.v

We no longer need to redefine `refine` (it now shelves by default).  Also clean up `constructor` a bit.
---
 theories/Compat/Coq84.v | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index d695ef1d89..5036b9bc85 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -21,16 +21,11 @@ Global Set Nonrecursive Elimination Schemes.
 (** See bug 3545 *)
 Global Set Universal Lemma Under Conjunction.
 
-(** In 8.5, [refine] leaves over dependent subgoals. *)
-Tactic Notation "refine" uconstr(term) := refine term; shelve_unifiable.
-
 (** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
-Ltac constructor_84 := constructor.
-Ltac constructor_84_n n := constructor n.
 Ltac constructor_84_tac tac := once (constructor; tac).
 
-Tactic Notation "constructor" := constructor_84.
-Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
+Tactic Notation "constructor" := Coq.Init.Notations.constructor.
+Tactic Notation "constructor" int_or_var(n) := Coq.Init.Notations.constructor n.
 Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
 
 (** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *)
-- 
cgit v1.2.3


From a585d46fbacfcc9cddf3da439e5f7001d429ba2a Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 5 Apr 2016 12:56:52 -0400
Subject: Fix bug #4656

I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd;
Coq.Init.Notations.constructor does not take any arguments.
---
 test-suite/bugs/closed/4656.v | 4 ++++
 theories/Compat/Coq84.v       | 4 ++--
 2 files changed, 6 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/4656.v

diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v
new file mode 100644
index 0000000000..c89a86d634
--- /dev/null
+++ b/test-suite/bugs/closed/4656.v
@@ -0,0 +1,4 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+Goal True.
+  constructor 1.
+Qed.
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 5036b9bc85..3266281922 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -22,10 +22,11 @@ Global Set Nonrecursive Elimination Schemes.
 Global Set Universal Lemma Under Conjunction.
 
 (** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
+Ltac constructor_84_n n := constructor n.
 Ltac constructor_84_tac tac := once (constructor; tac).
 
 Tactic Notation "constructor" := Coq.Init.Notations.constructor.
-Tactic Notation "constructor" int_or_var(n) := Coq.Init.Notations.constructor n.
+Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
 Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
 
 (** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *)
@@ -43,7 +44,6 @@ Tactic Notation "left" := left.
 Tactic Notation "eleft" := eleft.
 Tactic Notation "right" := right.
 Tactic Notation "eright" := eright.
-Tactic Notation "constructor" := constructor.
 Tactic Notation "econstructor" := econstructor.
 Tactic Notation "symmetry" := symmetry.
 Tactic Notation "split" := split.
-- 
cgit v1.2.3


From ab08345ebdb477bf4c83b46e0d8adc29296392f9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 5 Apr 2016 13:18:00 -0400
Subject: Add -compat 8.4 econstructor tactics, and tests

Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in
8.4.
---
 test-suite/success/Compat84.v | 19 +++++++++++++++++++
 theories/Compat/Coq84.v       |  9 ++++++++-
 2 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/success/Compat84.v

diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
new file mode 100644
index 0000000000..db6348fa17
--- /dev/null
+++ b/test-suite/success/Compat84.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+
+Goal True.
+  solve [ constructor 1 ]. Undo.
+  solve [ econstructor 1 ]. Undo.
+  solve [ constructor ]. Undo.
+  solve [ econstructor ]. Undo.
+  solve [ constructor (fail) ]. Undo.
+  solve [ econstructor (fail) ]. Undo.
+  split.
+Qed.
+
+Goal False \/ True.
+  solve [ constructor (constructor) ]. Undo.
+  solve [ econstructor (econstructor) ]. Undo.
+  solve [ constructor 2; constructor ]. Undo.
+  solve [ econstructor 2; econstructor ]. Undo.
+  right; esplit.
+Qed.
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 3266281922..d99d50996a 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -29,6 +29,14 @@ Tactic Notation "constructor" := Coq.Init.Notations.constructor.
 Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
 Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
 
+(** In 8.4, [econstructor (tac)] allowed backtracking across the use of [econstructor]; it has been subsumed by [econstructor; tac]. *)
+Ltac econstructor_84_n n := econstructor n.
+Ltac econstructor_84_tac tac := once (econstructor; tac).
+
+Tactic Notation "econstructor" := Coq.Init.Notations.econstructor.
+Tactic Notation "econstructor" int_or_var(n) := econstructor_84_n n.
+Tactic Notation "econstructor" "(" tactic(tac) ")" := econstructor_84_tac tac.
+
 (** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *)
 Tactic Notation "reflexivity" := reflexivity.
 Tactic Notation "assumption" := assumption.
@@ -44,7 +52,6 @@ Tactic Notation "left" := left.
 Tactic Notation "eleft" := eleft.
 Tactic Notation "right" := right.
 Tactic Notation "eright" := eright.
-Tactic Notation "econstructor" := econstructor.
 Tactic Notation "symmetry" := symmetry.
 Tactic Notation "split" := split.
 Tactic Notation "esplit" := esplit.
-- 
cgit v1.2.3


From f9ef1441083a988a938e163393dfbab04ab9da18 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 7 Apr 2016 13:52:03 +0200
Subject: Use -win32 and -win64 suffixes for installer name on Windows.

---
 dev/make-installer-win32.sh | 2 +-
 dev/make-installer-win64.sh | 2 +-
 dev/nsis/coq.nsi            | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh
index d405e66cc0..51d428dd1e 100755
--- a/dev/make-installer-win32.sh
+++ b/dev/make-installer-win32.sh
@@ -16,7 +16,7 @@ if [ ! -e bin/make.exe ]; then
 fi
 VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
 cd dev/nsis
-"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi
+"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win32" coq.nsi
 echo Installer:
 ls -h $PWD/*exe
 cd ../..
diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh
index 2f765c1a10..438f4ae5b7 100755
--- a/dev/make-installer-win64.sh
+++ b/dev/make-installer-win64.sh
@@ -22,7 +22,7 @@ if [ ! -e bin/make.exe ]; then
 fi
 VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
 cd dev/nsis
-"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi
+"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win64" coq.nsi
 echo Installer:
 ls -h $PWD/*exe
 cd ../..
diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
index 676490510c..e1052b1e1b 100755
--- a/dev/nsis/coq.nsi
+++ b/dev/nsis/coq.nsi
@@ -13,7 +13,7 @@ SetCompressor lzma
 
 !define MY_PRODUCT "Coq" ;Define your own software name here
 !define COQ_SRC_PATH "..\.."
-!define OUTFILE "coq-installer-${VERSION}.exe"
+!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe"
 
 !include "MUI2.nsh"
 !include "FileAssociation.nsh"
-- 
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(-)

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 +-
 test-suite/bugs/closed/2848.v | 7 ++++---
 toplevel/classes.ml           | 4 ++--
 toplevel/classes.mli          | 1 +
 4 files changed, 8 insertions(+), 6 deletions(-)

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"
diff --git a/test-suite/bugs/closed/2848.v b/test-suite/bugs/closed/2848.v
index de137d39d1..828e3b8c1f 100644
--- a/test-suite/bugs/closed/2848.v
+++ b/test-suite/bugs/closed/2848.v
@@ -2,8 +2,9 @@ Require Import Setoid.
 
 Parameter value' : Type.
 Parameter equiv' : value' -> value' -> Prop.
-
+Axiom cheat : forall {A}, A.
 Add Parametric Relation : _ equiv'
-  reflexivity proved by (Equivalence.equiv_reflexive _)
-  transitivity proved by (Equivalence.equiv_transitive _)
+  reflexivity proved by (Equivalence.equiv_reflexive cheat)
+  transitivity proved by (Equivalence.equiv_transitive cheat)
     as apply_equiv'_rel.
+Check apply_equiv'_rel : PreOrder equiv'.
\ No newline at end of file
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5f73b70a2e..653b4695ce 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -119,7 +119,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty
     instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
-let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
     ?(generalize=true)
     ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
@@ -290,7 +290,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
 	  declare_instance_constant k pri global imps ?hook id pl
             poly evm (Option.get term) termtype
-	else if Flags.is_program_mode () || !refine_instance || Option.is_empty term then begin
+	else if Flags.is_program_mode () || refine || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	    if Flags.is_program_mode () then
 	      let hook vis gr _ =
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index d600b3104f..f51e70388e 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -41,6 +41,7 @@ val declare_instance_constant :
 val new_instance :
   ?abstract:bool -> (** Not abstract by default. *)
   ?global:bool -> (** Not global by default. *)
+  ?refine:bool -> (** Allow refinement *)
   Decl_kinds.polymorphic ->
   local_binder list ->
   typeclass_constraint ->
-- 
cgit v1.2.3


From 17c9a9775e99d1551bf6d346d731271e3ae34417 Mon Sep 17 00:00:00 2001
From: Daniel de Rauglaudre
Date: Fri, 8 Apr 2016 14:53:32 +0200
Subject: Fixing a source of inefficiency and an artificial dependency in the
 printer in the congruence tactic.

Debugging messages were always built even when not in the verbose mode
of congruence.
---
 plugins/cc/ccalgo.ml  | 28 ++++++++++++++--------------
 plugins/cc/ccalgo.mli |  2 +-
 plugins/cc/ccproof.ml | 12 ++++++------
 plugins/cc/cctac.ml   |  8 ++++----
 4 files changed, 25 insertions(+), 25 deletions(-)

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc3d9ed560..5d16edfc6a 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,7 +25,7 @@ let init_size=5
 let cc_verbose=ref false
 
 let debug x =
-  if !cc_verbose then msg_debug x
+  if !cc_verbose then msg_debug (x ())
 
 let _=
   let gdopt=
@@ -603,7 +603,7 @@ let add_inst state (inst,int_subst) =
   Control.check_for_interrupt ();
   if state.rew_depth > 0 then
   if is_redundant state inst.qe_hyp_id int_subst then
-    debug (str "discarding redundant (dis)equality")
+    debug (fun () -> str "discarding redundant (dis)equality")
   else
     begin
       Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -618,7 +618,7 @@ let add_inst state (inst,int_subst) =
 	    state.rew_depth<-pred state.rew_depth;
 	    if inst.qe_pol then
 	      begin
-		debug (
+		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
 	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
 			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
@@ -626,7 +626,7 @@ let add_inst state (inst,int_subst) =
 	      end
 	    else
 	      begin
-		debug (
+		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
 	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
 			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
@@ -657,7 +657,7 @@ let join_path uf i j=
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (str "Linking " ++ pr_idx_term state.uf i1 ++
+  debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++
 		 str " and " ++ pr_idx_term state.uf i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
@@ -698,7 +698,7 @@ let union state i1 i2 eq=
 
 let merge eq state = (* merge and no-merge *)
   debug
-    (str "Merging " ++ pr_idx_term state.uf eq.lhs ++
+    (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++
        str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
   let uf=state.uf in
   let i=find uf eq.lhs
@@ -711,7 +711,7 @@ let merge eq state = (* merge and no-merge *)
 
 let update t state = (* update 1 and 2 *)
   debug
-    (str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
+    (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
   let rep = get_representative state.uf i in
@@ -773,7 +773,7 @@ let process_constructor_mark t i rep pac state =
 
 let process_mark t m state =
   debug
-    (str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
+    (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
     match m with
@@ -794,7 +794,7 @@ let check_disequalities state =
           else (str "No", check_aux q)
         in
         let _ = debug
-        (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
+        (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
          pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
         ans
     | [] -> None
@@ -979,7 +979,7 @@ let find_instances state =
   let pb_stack= init_pb_stack state in
   let res =ref [] in
   let _ =
-    debug (str "Running E-matching algorithm ... ");
+    debug (fun () -> str "Running E-matching algorithm ... ");
     try
       while true do
 	Control.check_for_interrupt ();
@@ -990,7 +990,7 @@ let find_instances state =
     !res
 
 let rec execute first_run state =
-  debug (str "Executing ... ");
+  debug (fun () -> str "Executing ... ");
   try
     while
       Control.check_for_interrupt ();
@@ -1000,7 +1000,7 @@ let rec execute first_run state =
 	None ->
 	  if not(Int.Set.is_empty state.pa_classes) then
 	    begin
-	      debug (str "First run was incomplete, completing ... ");
+	      debug (fun () -> str "First run was incomplete, completing ... ");
 	      complete state;
 	      execute false state
 	    end
@@ -1015,12 +1015,12 @@ let rec execute first_run state =
 		  end
 		else
 	      begin
-		debug (str "Out of instances ... ");
+		debug (fun () -> str "Out of instances ... ");
 		None
 	      end
 	    else
 	      begin
-		debug (str "Out of depth ... ");
+		debug (fun () -> str "Out of depth ... ");
 		None
 	      end
       | Some dis -> Some
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index b73c8eef86..c7fa2f56fd 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -120,7 +120,7 @@ val term_equal : term -> term -> bool
 
 val constr_of_term : term -> constr
 
-val debug : Pp.std_ppcmds -> unit
+val debug : (unit -> Pp.std_ppcmds) -> unit
 
 val forest : state -> forest
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index c188bf3bc9..d2bbaf6a7d 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -93,13 +93,13 @@ let pinject p c n a =
    p_rule=Inject(p,c,n,a)}
 
 let rec equal_proof uf i j=
-  debug (str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
   if i=j then prefl (term uf i) else
     let (li,lj)=join_path uf i j in
     ptrans (path_proof uf i li) (psym (path_proof uf j lj))
       
 and edge_proof uf ((i,j),eq)=
-  debug (str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  debug (fun () -> str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
   let pi=equal_proof uf i eq.lhs in
   let pj=psym (equal_proof uf j eq.rhs) in
   let pij=
@@ -115,7 +115,7 @@ and edge_proof uf ((i,j),eq)=
   ptrans (ptrans pi pij) pj
   
 and constr_proof uf i ipac=
-  debug (str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
+  debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
   let t=find_oldest_pac uf i ipac in
   let eq_it=equal_proof uf i t in
   if ipac.args=[] then
@@ -128,20 +128,20 @@ and constr_proof uf i ipac=
     ptrans eq_it (pcongr p (prefl targ))
       
 and path_proof uf i l=
-  debug (str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
+  debug (fun () -> str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
 	   (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
   match l with
   | [] -> prefl (term uf i)
   | x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x)
     
 and congr_proof uf i j=
-  debug (str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
   let (i1,i2) = subterms uf i
   and (j1,j2) = subterms uf j in
   pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2)
     
 and ind_proof uf i ipac j jpac=
-   debug (str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+   debug (fun () -> str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
   let p=equal_proof uf i j
   and p1=constr_proof uf i ipac
   and p2=constr_proof uf j jpac in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 0baa533704..df4a7319ac 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -413,16 +413,16 @@ let build_term_to_complete uf meta pac =
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.nf_enter begin fun gl ->
     Coqlib.check_required_library Coqlib.logic_module_name;
-    let _ = debug (Pp.str "Reading subgoal ...") in
+    let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
     let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
-    let _ = debug (Pp.str "Problem built, solving ...") in
+    let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
     let sol = execute true state in
-    let _ = debug (Pp.str "Computation completed.") in
+    let _ = debug (fun () -> Pp.str "Computation completed.") in
     let uf=forest state in
     match sol with
       None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
     | Some reason ->
-	debug (Pp.str "Goal solved, generating proof ...");
+	debug (fun () -> Pp.str "Goal solved, generating proof ...");
 	match reason with
 	  Discrimination (i,ipac,j,jpac) ->
 	    let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
-- 
cgit v1.2.3


From 84f079fa31723b6a97edc50ca7a81e1eb19e759c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 7 Apr 2016 20:31:42 +0200
Subject: Added compatibility coercions from Specif.v which were present in Coq
 8.4.

---
 theories/Compat/Coq84.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index d99d50996a..5c60966f28 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -76,3 +76,11 @@ End Coq.
 
 (** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *)
 Require Coq.Numbers.Natural.Peano.NPeano.
+
+(** The following coercions were declared by default in Specif.v. *)
+Coercion sig_of_sig2 : sig2 >-> sig.
+Coercion sigT_of_sigT2 : sigT2 >-> sigT.
+Coercion sigT_of_sig : sig >-> sigT.
+Coercion sig_of_sigT : sigT >-> sig.
+Coercion sigT2_of_sig2 : sig2 >-> sigT2.
+Coercion sig2_of_sigT2 : sigT2 >-> sig2.
-- 
cgit v1.2.3