Merge branch 'trunk' into located_switch

14 files changed, 7 insertions, 52 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 251e0d27db..9e0a2a03eb 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/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 5cc9d0df95..5a717f1662 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/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/logic.ml b/proofs/logic.ml
index e6024785db..54345abd97 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
@@ -379,7 +374,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)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 89aa32643b..1bf65b8aed 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
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 32eb9a3c1a..2396db868b 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
@@ -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)
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index b0b0eba08d..52bbd9ac56 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
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/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
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5c7659ac0e..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
 
@@ -162,31 +161,11 @@ let tclMAP tacfun l =
 
 (* 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 =
   let rslt = tac ptree in
   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..e179589df2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -119,10 +119,8 @@ 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
-val tclNOTSAMEGOAL   : tactic -> tactic
 
 (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
    if it succeeds, applies [tac2] to the resulting subgoals,
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
 
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. *)