Removing unused parts of the Goal.sensitive monad.

Some legacy code remains to keep the newish refine tactic working, but
ultimately it should be removed. I did not manage to do it properly though,
i.e. without breaking the test-suite furthermore.

1 files changed, 19 insertions, 108 deletions

diff --git a/proofs/goal.mli b/proofs/goal.mli
index 988853382..535a2f2b1 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -42,112 +42,6 @@ val equal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
    non-unifiable goals. *)
 val partition_unifiable : Evd.evar_map -> goal list -> goal list * goal list
 
-(*** Goal tactics ***)
-
-
-(* Goal tactics are [subgoal sensitive]-s *)
-type subgoals = private { subgoals: goal list }
-
-(* Goal sensitive values *)
-type +'a sensitive
-
-(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
-val eval :
-  'a sensitive -> Environ.env -> Evd.evar_map -> goal ->
-    'a * Evd.evar_map
-
-(* monadic bind on sensitive expressions *)
-val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive
-
-(* monadic return on sensitive expressions *)
-val return : 'a -> 'a sensitive
-
-
-(* interpretation of "open" constr *)
-(* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. 
-    In an ideal world, this could/should be the other way round.
-    As of now, though, it seems at least quite useful to build tactics. *)
-val interp_constr : Constrexpr.constr_expr -> Term.constr sensitive
-
-(* Type of constr with holes used by refine. *)
-type refinable
-
-module Refinable : sig
-  type t = refinable 
-  type handle
-
-  val make : (handle -> Term.constr sensitive) -> refinable sensitive
-  val make_with : (handle -> (Term.constr*'a) sensitive) -> (refinable*'a) sensitive
-
-  val mkEvar : handle -> Environ.env -> Term.types -> Term.constr sensitive
-
-  (* [with_type c typ] constrains term [c] to have type [typ].  *)
-  val with_type : Term.constr -> Term.types -> Term.constr sensitive
-
-  val resolve_typeclasses : ?filter:Typeclasses.evar_filter -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
-
-
-  (* [constr_of_open_constr h check_type] transforms an open constr into a 
-     goal-sensitive constr, adding the undefined variables to the set of subgoals.
-     If [check_type] is true, the term is coerced to the conclusion of the goal.
-     It allows to do refinement with already-built terms with holes.
-  *)
-  val constr_of_open_constr : handle -> bool -> Evd.open_constr -> Term.constr sensitive
-
-end
-
-(* [refine t] takes a refinable term and use it as a partial proof for current
-    goal. *)
-val refine : refinable -> subgoals sensitive
-
-
-(*** Cleaning  goals ***)
-
-(* Implements the [clear] tactic *)
-val clear : Names.Id.Set.t -> subgoals sensitive
-
-(* Implements the [clearbody] tactic *)
-val clear_body : Names.Id.t list -> subgoals sensitive
-
-
-(*** Conversion in goals ***)
-
-(* Changes an hypothesis of the goal with a convertible type and body.
-   Checks convertibility if the boolean argument is true. *)
-val convert_hyp : bool -> Context.named_declaration -> subgoals sensitive
-
-(* Changes the conclusion of the goal with a convertible type and body.
-   Checks convertibility if the boolean argument is true. *)
-val convert_concl : bool -> Term.constr -> subgoals sensitive
-
-(*** Bureaucracy in hypotheses ***)
-
-(* Renames a hypothesis. *)
-val rename_hyp : Names.Id.t -> Names.Id.t -> subgoals sensitive
-
-(*** Sensitive primitives ***)
-
-(* representation of the goal in form of an {!Evd.evar_info} *)
-val info : Evd.evar_info sensitive
-
-(* [concl] is the conclusion of the current goal *)
-val concl : Term.constr sensitive
-
-(* [hyps] is the [named_context_val] representing the hypotheses
-   of the current goal *)
-val hyps : Environ.named_context_val sensitive
-
-(* [env] is the current [Environ.env] containing both the 
-   environment in which the proof is ran, and the goal hypotheses *)
-val env : Environ.env sensitive
-
-(* [defs] is the [Evd.evar_map] at the current evaluation point *)
-val defs : Evd.evar_map sensitive
-
-(* [enter] combines [env], [defs], [hyps] and [concl] in a single
-   primitive. *)
-val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive
-
 (* Layer to implement v8.2 tactic engine ontop of the new architecture. 
    Types are different from what they used to be due to a change of the
    internal types. *)
@@ -220,6 +114,23 @@ module V82 : sig
   (* Goal represented as a type, doesn't take into account section variables *)
   val abstract_type : Evd.evar_map -> goal -> Term.types 
 
-  val to_sensitive : (goal Evd.sigma -> 'a) -> 'a sensitive
-  val change_evar_map : Evd.evar_map -> unit sensitive
 end
+
+(*** Goal tactics. DEPRECATED. ***)
+
+(* Goal tactics are [subgoal sensitive]-s *)
+type subgoals = private { subgoals: goal list }
+
+(* Goal sensitive values *)
+type +'a sensitive
+
+(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
+val eval :
+  'a sensitive -> Environ.env -> Evd.evar_map -> goal ->
+    'a * Evd.evar_map
+
+val refine_open_constr : Evd.open_constr -> subgoals sensitive
+
+(* [enter] combines [env], [defs], [hyps] and [concl] in a single
+   primitive. *)
+val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive