A few more comments in tactics.mli and hippatern.ml.

2 files changed, 27 insertions, 14 deletions

diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index dc78229f68..e171c21474 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -274,6 +274,11 @@ let match_with_equation t =
         else raise NoEquationFound
     | _ -> raise NoEquationFound
 
+(* Note: An "equality type" is any type with a single argument-free
+   constructor: it captures eq, eq_dep, JMeq, eq_true, etc. but also
+   True/unit which is the degenerate equality type (isomorphic to ()=());
+   in particular, True/unit are provable by "reflexivity" *)
+
 let is_inductive_equality ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let nconstr = Array.length mip.mind_consnames in
@@ -287,6 +292,8 @@ let match_with_equality_type t =
 
 let is_equality_type t = op2bool (match_with_equality_type t)
 
+(* Arrows/Implication/Negation *)
+
 let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
 
 let match_arrow_pattern t =
@@ -296,6 +303,13 @@ let match_arrow_pattern t =
       assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
     | _ -> anomaly (Pp.str "Incorrect pattern matching")
 
+let match_with_imp_term c=
+  match kind_of_term c with
+    | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b)
+    | _              -> None
+
+let is_imp_term c = op2bool (match_with_imp_term c)
+
 let match_with_nottype t =
   try
     let (arg,mind) = match_arrow_pattern t in
@@ -304,6 +318,8 @@ let match_with_nottype t =
 
 let is_nottype t = op2bool (match_with_nottype t)
 
+(* Forall *)
+
 let match_with_forall_term c=
   match kind_of_term c with
     | Prod (nam,a,b) -> Some (nam,a,b)
@@ -311,13 +327,6 @@ let match_with_forall_term c=
 
 let is_forall_term c = op2bool (match_with_forall_term c)
 
-let match_with_imp_term c=
-  match kind_of_term c with
-    | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b)
-    | _              -> None
-
-let is_imp_term c = op2bool (match_with_imp_term c)
-
 let match_with_nodep_ind t =
   let (hdapp,args) = decompose_app t in
     match (kind_of_term hdapp) with
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 53dfed2cbc..b974f341f1 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -110,7 +110,7 @@ val intro_patterns_bound_to : int -> Id.t move_location ->
 val intro_pattern_to : Id.t move_location -> intro_pattern_expr ->
   unit Proofview.tactic
 
-(** Implements "intros", with [] standing for "**" *)
+(** Implements user-level "intros", with [] standing for "**" *)
 val intros_patterns : intro_pattern_expr located list -> unit Proofview.tactic
 
 (** {6 Exact tactics. } *)
@@ -197,7 +197,6 @@ val apply_in :
 
 (** {6 Elimination tactics. } *)
 
-
 (*
    The general form of an induction principle is the following:
 
@@ -244,7 +243,6 @@ type elim_scheme = {
   farg_in_concl: bool;     (** true if (f...) appears at the end of conclusion *)
 }
 
-
 val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme
 
 (** elim principle with the index of its inductive arg *)
@@ -290,6 +288,8 @@ val destruct : evars_flag ->
 
 (** {6 Generic case analysis / induction tactics. } *)
 
+(** Implements user-level "destruct" and "induction" *)
+
 val induction_destruct : rec_flag -> evars_flag ->
   ((evar_map * constr with_bindings) induction_arg *
   (intro_pattern_naming_expr located option *
@@ -303,7 +303,7 @@ val induction_destruct : rec_flag -> evars_flag ->
 val case_type         : types -> unit Proofview.tactic
 val elim_type         : types -> unit Proofview.tactic
 
-(** {6 Introduction tactics. } *)
+(** {6 Constructor tactics. } *)
 
 val constructor_tac      : evars_flag -> int option -> int ->
   constr bindings -> unit Proofview.tactic
@@ -322,7 +322,7 @@ val simplest_left        : unit Proofview.tactic
 val simplest_right       : unit Proofview.tactic
 val simplest_split       : unit Proofview.tactic
 
-(** {6 Logical connective tactics. } *)
+(** {6 Equality tactics. } *)
 
 val setoid_reflexivity : unit Proofview.tactic Hook.t
 val reflexivity_red             : bool -> unit Proofview.tactic
@@ -389,6 +389,8 @@ val new_generalize_gen  : ((occurrences * constr) * Name.t) list -> unit Proofvi
 
 val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -> tactic
 
+(** {6 Other tactics. } *)
+
 val unify           : ?state:Names.transparent_state -> constr -> constr -> tactic
 
 val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
@@ -404,12 +406,13 @@ val general_rewrite_clause :
 val subst_one :
   (bool -> Id.t -> Id.t * constr * bool -> unit Proofview.tactic) Hook.t
 
-
 val declare_intro_decomp_eq :
   ((int -> unit Proofview.tactic) -> Coqlib.coq_eq_data * types *
    (types * constr * constr) ->
    constr * types -> unit Proofview.tactic) -> unit
 
+(** {6 Simple form of basic tactics. } *)
+
 module Simple : sig
   (** Simplified version of some of the above tactics *)
 
@@ -425,7 +428,8 @@ module Simple : sig
 
 end
 
-(** Tacticals defined directly in term of Proofview *)
+(** {6 Tacticals defined directly in term of Proofview} *)
+
 module New : sig
 
   val refine : Evd.open_constr -> unit Proofview.tactic