detail: update text of some debug flags

Author: fblanqui

src/handle/inductive.ml

@@ -16,7 +16,7 @@ open Core open Term open Print
 open Parsing open Syntax
 
 (** Logging function for generating of inductive principle. *)
-let log_ind = Logger.make 'g' "indu" "induction principles generation"
+let log_ind = Logger.make 'g' "indu" "generation of induction principles"
 let log_ind = log_ind.pp
 
 (** Type for inductive type definitions. *)

src/handle/rewrite.ml

@@ -6,7 +6,7 @@ open Core open Term open Print
 open Goal
 
 (** Logging function for the rewrite tactic. *)
-let log = Logger.make 'r' "rewr" "the rewrite tactic"
+let log = Logger.make 'r' "rewr" "rewrite tactic"
 let log = log.pp
 
 (** Equality configuration. *)

src/handle/why3_tactic.ml

@@ -8,7 +8,7 @@ open Fol
 open Goal
 
 (** Logging function for external prover calling with Why3. *)
-let log = Logger.make 'y' "why3" "why3 provers"
+let log = Logger.make 'y' "why3" "why3 tactic"
 let log = log.pp
 
 (** [default_prover] contains the name of the current prover. Note that it can

src/parsing/scope.ml

@@ -10,7 +10,7 @@ open Core open Term open Env open Sig_state open Print
 let term = Raw.term
 
 (** Logging function for term scoping. *)
-let log_scop = Logger.make 'o' "scop" "term scoping"
+let log_scop = Logger.make 'o' "scop" "scoping"
 let log_scop = log_scop.pp
 
 (** [find_qid ~find_sym prt prv ss env qid] returns a boxed term corresponding