From fe99efdbe409e47f20776c62a76d4de7f0188afc Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 11 Apr 2017 12:46:23 +0200
Subject: Update various comments to use "template polymorphism"

Also remove obvious comments.
---
 proofs/logic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index e6024785db..d8c1f1f3b5 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -379,7 +379,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	let (acc',hdty,sigma,applicand) =
 	  if is_template_polymorphic env sigma (EConstr.of_constr f) then
 	    let ty = 
-	      (* Template sort-polymorphism of definition and inductive types *)
+	      (* Template polymorphism of definitions and inductive types *)
 	      let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
 	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
 	        type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args)
-- 
cgit v1.2.3


From 552544a3d385a3a59def038bdb0a22a69fe4b0a9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Mar 2017 16:42:24 +0100
Subject: Removing the tclNOTSAMEGOAL primitive from the API.

The only use in Equality is reimplemented in the new engine.
---
 proofs/refiner.ml  | 13 -------------
 proofs/refiner.mli |  1 -
 2 files changed, 14 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5c7659ac0e..d086f0bbca 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -174,19 +174,6 @@ let tclPROGRESS tac ptree =
   if Goal.V82.progress rslt ptree then rslt
   else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.")
 
-(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
-   one of them being identical to the original goal *)
-let tclNOTSAMEGOAL (tac : tactic) goal =
-  let same_goal gls1 evd2 gl2 =
-    Goal.V82.same_goal gls1.sigma gls1.it evd2 gl2
-  in
-  let rslt = tac goal in
-  let {it=gls;sigma=sigma} = rslt in
-  if List.exists (same_goal goal sigma) gls
-  then user_err ~hdr:"Refiner.tclNOTSAMEGOAL"
-      (str"Tactic generated a subgoal identical to the original goal.")
-  else rslt
-
 (* Execute tac, show the names of new hypothesis names created by tac
    in the "as" format and then forget everything. From the logical
    point of view [tclSHOWHYPS tac] is therefore equivalent to idtac,
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 56f5facf89..de6502dc36 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -122,7 +122,6 @@ val tclDO            : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
-val tclNOTSAMEGOAL   : tactic -> tactic
 
 (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
    if it succeeds, applies [tac2] to the resulting subgoals,
-- 
cgit v1.2.3


From 21ee9a82807176acecf917e2a1e6074bed1c88ff Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Mar 2017 18:16:27 +0100
Subject: Removing the tclWEAK_PROGRESS tactical.

The only remaining use was applied on the unfold tactic, and the behaviours
of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced
by their argument tactic.
---
 proofs/goal.mli    | 3 ---
 proofs/refiner.ml  | 7 -------
 proofs/refiner.mli | 1 -
 3 files changed, 11 deletions(-)

(limited to 'proofs')

diff --git a/proofs/goal.mli b/proofs/goal.mli
index a2fa34c05e..ee2e736120 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -59,9 +59,6 @@ module V82 : sig
      second goal *)
   val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
 
-  (* Principal part of the weak-progress tactical *)
-  val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-   
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
     
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index d086f0bbca..bc12b3ba71 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -160,13 +160,6 @@ let rec tclTHENLIST = function
 let tclMAP tacfun l =
   List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
 
-(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
-the goal unchanged *)
-let tclWEAK_PROGRESS tac ptree =
-  let rslt = tac ptree in
-  if Goal.V82.weak_progress rslt ptree then rslt
-  else user_err ~hdr:"Refiner.WEAK_PROGRESS" (str"Failed to progress.")
-
 (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
 the goal unchanged *)
 let tclPROGRESS tac ptree =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index de6502dc36..e179589df2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -119,7 +119,6 @@ val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> Pp.std_ppcmds -> tactic
 val tclFAIL_lazy     : int -> Pp.std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
 
-- 
cgit v1.2.3


From fa27856d2d4ac0f55b99b9406b74301057deb0aa Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Thu, 27 Apr 2017 09:57:09 +0200
Subject: contracting the type of "Pfedit.solve_by_implicit_tactic"

---
 proofs/pfedit.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f9fb0b76de..7622a87768 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
 val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr) option
+val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
-- 
cgit v1.2.3


From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:36:45 +0200
Subject: Fix omitted labels in function calls

---
 proofs/redexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 0fe5c73f15..cb35384227 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -43,7 +43,7 @@ let cbv_native env sigma c =
 
 let whd_cbn flags env sigma t =
   let (state,_) =
-    (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
+    (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty))
   in
   Reductionops.Stack.zip ~refold:true sigma state
 
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 proofs/clenv.ml   | 5 -----
 proofs/logic.ml   | 5 -----
 proofs/tacmach.ml | 3 ---
 3 files changed, 13 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f9ebc42330..605914a015 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -27,11 +27,6 @@ open Unification
 open Misctypes
 open Sigma.Notations
 
-(* Abbreviations *)
-
-let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
-
 (******************************************************************)
 (* Clausal environments *)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e6024785db..9ab8c34d89 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -97,11 +97,6 @@ let check_typability env sigma c =
    (instead of iterating on the list of identifier to be removed, which
    forces the user to give them in order). *)
 
-let clear_hyps env sigma ids sign cl =
-  let evdref = ref (Evd.clear_metas sigma) in
-  let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in
-  (hyps, cl, !evdref)
-
 let clear_hyps2 env sigma ids sign t cl =
   let evdref = ref (Evd.clear_metas sigma) in
   let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b55f8ef113..97c5cda770 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -179,9 +179,6 @@ module New = struct
   let pf_unsafe_type_of gl t =
     pf_apply unsafe_type_of gl t
 
-  let pf_get_type_of gl t =
-    pf_apply (Retyping.get_type_of ~lax:true) gl t
-
   let pf_type_of gl t =
     pf_apply type_of gl t
 
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 proofs/clenvtac.mli   | 1 -
 proofs/goal.ml        | 1 -
 proofs/proof_type.mli | 3 ---
 proofs/refiner.ml     | 1 -
 proofs/tacmach.mli    | 1 -
 5 files changed, 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 5b7164705a..26069207eb 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -8,7 +8,6 @@
 
 (** Legacy components of the previous proof engine. *)
 
-open Term
 open Clenv
 open EConstr
 open Unification
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 9046f45341..fc8e635a07 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Pp
-open Term
 open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 03bc5e4710..e59db9e427 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -11,9 +11,6 @@
 open Evd
 open Names
 open Term
-open Glob_term
-open Nametab
-open Misctypes
 
 (** This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index bc12b3ba71..259e96a276 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open Evd
-open Environ
 open Proof_type
 open Logic
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 627a8e0e7e..e6e60e27f7 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -15,7 +15,6 @@ open Proof_type
 open Redexpr
 open Pattern
 open Locus
-open Misctypes
 
 (** Operations for handling terms under a local typing context. *)
 
-- 
cgit v1.2.3


From c1bf3bc4956d0b8af879fcf4854cbd650e1821c0 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 20 May 2017 14:06:06 +0200
Subject: Change wrong bullet message.

Remove a space before colon.
Remove the use of term mandatory
(this closes https://coq.inria.fr/bugs/show_bug.cgi?id=3994).
---
 proofs/proof_global.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5f4a7766f3..99fab08486 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -516,7 +516,7 @@ module Bullet = struct
       | NeedClosingBrace -> str"Try unfocusing with \"}\"."
       | NoBulletInUse -> assert false (* This should never raise an error. *)
       | ProofFinished -> str"No more subgoals."
-      | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here."
+      | Suggest b -> str"Expecting " ++ pr_bullet b ++ str"."
       | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished."
 
     exception FailedBullet of t * suggestion
@@ -525,7 +525,7 @@ module Bullet = struct
       CErrors.register_handler
 	(function
 	| FailedBullet (b,sugg) ->
-	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
+	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str": " in
 	  CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
 	| _ -> raise CErrors.Unhandled)
 
-- 
cgit v1.2.3


From c1e9a27d383688e44ba34ada24fe08151cb5846e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 21:04:18 +0200
Subject: [vernac] Remove `Save thm id.` command.

We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:

```
Goal Type.
⋮
Save id.
```

has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.

We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.

It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
---
 proofs/proof_global.ml  | 2 +-
 proofs/proof_global.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5f4a7766f3..0443d6357f 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -82,7 +82,7 @@ type proof_object = {
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
   | Proved of Vernacexpr.opacity_flag *
-             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              Vernacexpr.lident option *
               proof_object
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6bb6f5e2cb..e90fb5bc93 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -70,7 +70,7 @@ type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
 		  proof_universes
   | Proved of Vernacexpr.opacity_flag *
-             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              Vernacexpr.lident option *
               proof_object
 type proof_terminator
 type closed_proof = proof_object * proof_terminator
-- 
cgit v1.2.3