update descriptions

src/core/printer.ml

@@ -215,7 +215,7 @@ let meta_remove_logic = register_meta "remove_logic" [MTlsymbol]
          Used@ in@ bisection."
 
 let meta_realized_theory = register_meta "realized_theory" [MTstring; MTstring]
-  ~desc:"Specify@ that@ a@ Why3@ theory@ is@ \"realized\"@ as@ a@ module@ \
+  ~desc:"Specify@ that@ a@ Why3@ theory@ is@ realized@ as@ a@ module@ \
          in@ an@ ITP."
 
 let check_syntax_type ts s = check_syntax s (List.length ts.ts_args)

src/core/trans.ml

@@ -17,7 +17,8 @@ open Theory
 open Task
 
 let debug = Debug.register_info_flag "transform"
-  ~desc:"Be@ verbose@ about@ application@ of@ proof@ task@ transformations."
+  ~desc:"Print@ debugging@ messages@ about@ application@ \
+         of@ proof@ task@ transformations."
 
 (** Task transformation *)
 

src/driver/autodetection.ml

@@ -46,7 +46,8 @@ module Wc = Whyconf
 open Rc
 
 let debug = Debug.register_info_flag "autodetect"
-  ~desc:"Be@ verbose@ about@ autodetection@ of@ external@ provers."
+  ~desc:"Print@ debugging@ messages@ about@ auto-detection@ \
+         of@ external@ provers."
 
 (* auto-detection of provers *)
 

src/driver/call_provers.ml

@@ -113,7 +113,8 @@ let rec grep out l = match l with
 
 
 let debug = Debug.register_info_flag "call_prover"
-  ~desc:"Be@ verbose@ about@ prover@ calls@ and@ keep@ temporary@ files."
+  ~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
+         and@ keep@ temporary@ files."
 
 type post_prover_call = unit -> prover_result
 

src/parser/glob.ml

@@ -11,8 +11,8 @@
 
 open Ident
 
-let flag = Debug.register_flag "track_use"
-  ~desc:"Track@ use/clone@ instructions.@ Used@ by@ why3doc."
+let flag = Debug.register_flag "track_symbol_use"
+  ~desc:"Track@ symbol@ occurrences@ in@ source@ files.@ Used@ by@ why3doc."
 
 let () = Debug.unset_flag flag (* make sure it is unset by default *)
 

src/parser/typing.ml

@@ -73,9 +73,9 @@ let () = Exn_printer.register (fun fmt e -> match e with
   | _ -> raise e)
 
 let debug_parse_only = Debug.register_flag "parse_only"
-  ~desc:"Stop@ after@ the@ parsing."
+  ~desc:"Stop@ after@ parsing."
 let debug_type_only  = Debug.register_flag "type_only"
-  ~desc:"Stop@ after@ the@ typing."
+  ~desc:"Stop@ after@ type-checking."
 
 (** Environments *)
 

src/printer/alt_ergo.ml

@@ -20,10 +20,11 @@ open Decl
 open Printer
 
 let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol]
-  ~desc:"Specify that a symbol is associative and commutative."
+  ~desc:"Specify@ that@ a@ symbol@ is@ associative@ and@ commutative."
+
 let meta_printer_option =
   Theory.register_meta "printer_option" [Theory.MTstring]
-    ~desc:"Some paramters given to the printer."
+    ~desc:"Pass@ additional@ parameters@ to@ the@ pretty-printer."
 
 type info = {
   info_syn : syntax_map;
@@ -366,7 +367,7 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task =
     (List.rev (Trans.apply print_decls task))
 
 let () = register_printer "alt-ergo" print_task
-  ~desc:"Printer for the alt-ergo theorem provers"
+  ~desc:"Printer for the Alt-Ergo theorem prover."
 (*
 let print_goal info fmt (id, f, task) =
   print_task info fmt task;

src/printer/gappa.ml

@@ -31,7 +31,8 @@ let syntactic_transform transf =
 let () =
   Trans.register_transform "abstract_unknown_lsymbols"
     (syntactic_transform Abstraction.abstraction)
-    ~desc:"Abstract@ applications@ of@ non-built-in@ symbols@ with@ constants.";
+    ~desc:"Abstract@ applications@ of@ non-built-in@ symbols@ with@ \
+      constants.@ Used@ by@ the@ Gappa@ pretty-printer.";
   Trans.register_transform "simplify_unknown_lsymbols"
     (syntactic_transform (fun check_ls -> Trans.goal (fun pr f ->
       [create_prop_decl Pgoal pr (Simplify_formula.fmla_cond_subst
@@ -45,8 +46,9 @@ let () =
           | Tapp(ls,_) -> not (check_ls ls)
           | _ -> true) f)
       ])))
-    ~desc:"Same@ as@ simplify_trivial_quantification_in_goal,@ but@ instead@ of@ substituting@ quantified@ variables,@ substitute@ applications@ of@ non-buit-in@ symbols.";
-
+    ~desc:"Same@ as@ simplify_trivial_quantification_in_goal,@ but@ instead@ \
+      of@ substituting@ quantified@ variables,@ substitute@ applications@ \
+      of@ non-buit-in@ symbols.@ Used@ by@ the@ Gappa@ pretty-printer."
 
 (* patterns (TODO: add a parser and generalize it out of Gappa) *)
 
@@ -91,13 +93,14 @@ let real_minus = ref ps_equ
 (** lsymbol, ""/"not ", op, rev_op *)
 let arith_meta = register_meta "gappa arith"
   [MTlsymbol;MTstring;MTstring;MTstring]
-  ~desc:"Specifies how to pretty-print symbols into gappa format:@\n  \
-@[\
- @[<hov 2>- first argument: which symbol@]@\n\
- @[<hov 2>- second argument: which prefix around the term@]@\n\
- @[<hov 2>- third argument: which operator to pretty-print@]@\n\
- @[<hov 2>- fourth argument: which is the inverse operator to pretty-print@]\
-@]"
+  ~desc:"Specify@ how@ to@ pretty-print@ arithmetic@ \
+          operations@ in@ the@ Gappa@ format:@\n  \
+    @[\
+     @[<hov 2>- first@ argument:@ the@ symbol@]@\n\
+     @[<hov 2>- second@ argument:@ the@ prefix@ to@ put@ before@ the@ term@]@\n\
+     @[<hov 2>- third@ argument:@ the@ operator@ to@ print@]@\n\
+     @[<hov 2>- fourth@ argument:@ the@ inverse@ operator@]\
+    @]"
 
 let find_th env file th =
   let theory = Env.find_theory env [file] th in

src/printer/smtv1.ml

@@ -223,4 +223,4 @@ let () = register_printer "smtv1"
   (fun _env pr thpr blacklist ?old:_ fmt task ->
      forget_all ident_printer;
      print_task pr thpr blacklist fmt task)
-  ~desc:"Printer@ for@ the@ smtlib@ version@ 1@ format."
+  ~desc:"Printer@ for@ the@ SMTlib@ version@ 1@ format."

src/printer/smtv2.ml

@@ -317,7 +317,7 @@ let () = register_printer "smtv2"
   (fun _env pr thpr blacklist ?old:_ fmt task ->
      forget_all ident_printer;
      print_task_old pr thpr blacklist fmt task)
-  ~desc:"Printer for the smtlib version 2 format."
+  ~desc:"Printer for the SMTlib version 2 format."
 
 (*
 let print_decls =
@@ -344,5 +344,5 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task =
     (List.rev (Trans.apply print_decls task))
 
 let () = register_printer "smtv2new" print_task
-  ~desc:"New (TODO: in which sense?) printer for the smtlib version 2 format."
+  ~desc:"Printer for the SMTlib version 2 format."
 *)

src/printer/why3printer.ml

@@ -386,8 +386,7 @@ let print_task_old _env pr thpr _blacklist ?old:_ fmt task =
   fprintf fmt "theory Task@\n%a@\nend@."
     (print_list nothing print_tdecl) (Task.task_tdecls task)
 
-let () = register_printer "why3old" print_task_old
-  ~desc:"TODO"
+let () = register_printer "why3old" print_task_old ~desc:""
 *)
 
 let print_tdecls =
@@ -406,5 +405,5 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task =
       (List.rev (Trans.apply print_tdecls task))
 
 let () = register_printer "why3" print_task
-  ~desc:"Printer@ for@ the@ logical@ format@ of@ Why3,@ \
-    used@ for@ debugging@ purposes."
+  ~desc:"Printer@ for@ the@ logical@ format@ of@ Why3.@ \
+    Used@ for@ debugging."

src/session/session.ml

@@ -25,7 +25,8 @@ module C = Whyconf
 module Tc = Termcode
 
 let debug = Debug.register_info_flag "session"
-  ~desc:"About the why3 session creation, reading and writing."
+  ~desc:"Pring@ debugging@ messages@ about@ Why3@ session@ \
+         creation,@ reading@ and@ writing."
 
 (** {2 Type definitions} *)
 

src/session/session_scheduler.ml

@@ -14,8 +14,8 @@ open Session
 open Debug
 
 let debug = register_info_flag "scheduler"
-  ~desc:"About@ the@ session@ scheduler@ which@ schedules@ the@ application@ \
-          of@ transformtions@ or@ the@ call@ of@ provers."
+  ~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls@ \
+         and@ transformtion@ applications."
 
 (***************************)
 (*     main functor        *)

src/session/termcode.ml

@@ -24,9 +24,8 @@ let string_of_shape x = x
 let shape_of_string x = x
 
 let debug = Debug.register_info_flag "session_pairing"
-  ~desc:"About@ the@ way@ old@ goals@ recorded@ in@ sessions@ are@ paired@ \
-         with@ new@ goals@ obtained@ after@ modifications@ of@ the@ source@ \
-         file."
+  ~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
+         session@ trees@ after@ modification@ of@ source@ files."
 
 let current_shape_version = 2
 

src/session/xml.mll

@@ -9,10 +9,8 @@
 (*                                                                  *)
 (********************************************************************)
 
-
 {
-
-   type element =
+  type element =
     { name : string;
       attributes : (string * string) list;
       elements : element list;
@@ -44,7 +42,7 @@
   let parse_error s = raise (Parse_error s)
   open Debug
   let debug = register_info_flag "xml"
-    ~desc:"About the xml parsing."
+    ~desc:"Print@ the@ XML@ parser@ debugging@ messages."
 }
 
 let space = [' ' '\t' '\r' '\n']

src/transform/close_epsilon.ml

@@ -78,6 +78,6 @@ let close_epsilon =
     if used then Trans.decl close None else Trans.identity)
 
 let () = Trans.register_transform "close_epsilon" close_epsilon
-  ~desc:"TODO"
+  ~desc:"Beta-abstract free variables out of lambda-terms."
 
 (* TODO variable abstraction *)

src/transform/discriminate.ml

@@ -17,48 +17,43 @@ open Decl
 open Theory
 open Task
 
-let meta_inst   = register_meta "encoding : inst"   [MTty]
-  ~desc:"Specify@ which@ type@ should@ instantiate@ symbol@ marked@ by@ \
+let meta_inst = register_meta "encoding : inst" [MTty]
+  ~desc:"Specify@ which@ types@ should@ instantiate@ symbols@ marked@ by@ \
          'encoding : lskept'."
+
 let meta_lskept = register_meta "encoding : lskept" [MTlsymbol]
-  ~desc:"Specify@ which@ function@ symbols@ should@ be@ kept.@ If@ the@ \
-         function@ is@ polymorphic,@ the@ monorphisations@ which@ signatures@ \
-         contain@ only@ types@ @ marked@ with@ 'encoding : inst'@ are@ kept."
+  ~desc:"Specify@ which@ function/predicate@ symbols@ should@ be@ kept.@ \
+         When@ the@ symbol@ is@ polymorphic,@ generate@ every@ possible@ \
+         type@ insntance@ with@ types@ marked@ by@ 'encoding : inst'."
+
 let meta_lsinst = register_meta "encoding : lsinst" [MTlsymbol;MTlsymbol]
-  ~desc:"Specify@ which@ instantiations@ of@ symbols@ should@ be@ kept.@ \
-         The first@ symbol@ specifies@ the@ symbol,@ the@ signature@ of@ the@ \
-         second@ specifies@ the@ instantiation@ to@ keep."
-
-let meta_select_inst   = register_meta_excl "select_inst"   [MTstring]
-  ~desc:"@[Specify@ how@ to@ automatically@ mark@ type@ by@ \
-'encoding : inst':@]@\n  \
-@[\
-  - none:@[ don't@ mark@ automatically@]@\n\
-  - goal:@[ mark@ all@ the@ closed@ type@ that@ appear@ has@ argument@ \
-            in@ the@ goal@]@\n\
-  - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\
-@]"
+  ~desc:"Specify@ which@ type@ instances@ of@ symbols@ should@ be@ kept.@ \
+         The first@ symbol@ specifies@ the@ polymorphic@ symbol,@ \
+         the@ second@ provides@ a@ monomorphic@ type@ signature@ to@ keep."
+
+let meta_select_inst = register_meta_excl "select_inst" [MTstring]
+  ~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding : inst':@;  \
+    @[\
+      - none: @[don't@ mark@ any@ type@ automatically@]@\n\
+      - goal: @[mark@ every@ closed@ type@ in@ the@ goal@]@\n\
+      - all:  @[mark@ every@ closed@ type@ in@ the@ task.@]\
+    @]"
 
 let meta_select_lskept = register_meta_excl "select_lskept" [MTstring]
-  ~desc:"@[Specify@ how@ to@ automatically@ mark@ symbol@ by@ \
-'encoding : lskept':@]@\n  \
-@[\
-  - none:@[ don't@ mark@ automatically@]@\n\
-  - goal:@[ mark@ all@ the@ symbols@ acceptable@ that@ appear@ in@ the@ \
-            goal.@ The signature@ of an@ acceptable@ symbol@ contain@ at@ \
-            least@ one@ type@ that@ is@ not@ a@ type@ variable@ neither@]@\n\
-  - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\
-@]"
+  ~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding : lskept':@;  \
+    @[\
+      - none: @[don't@ mark@ any@ symbol@ automatically@]@\n\
+      - goal: @[mark@ every@ polymorphic@ symbol@ in@ the@ goal@]@\n\
+      - all:  @[mark@ every@ polymorphic@ symbol@ in@ the@ task.@]\
+    @]"
 
 let meta_select_lsinst = register_meta_excl "select_lsinst" [MTstring]
-  ~desc:"@[Specify@ how@ to@ automatically@ mark@ symbol@ by@ \
-'encoding : lskept':@]@\n  \
-@[\
-  - none:@[ don't@ mark@ automatically@]@\n\
-  - goal:@[ mark@ all@ the@ instantiation of symbols@ that@ appear@ in@ \
-             the@ goal@]@\n\
-  - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\
-@]"
+  ~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding : lsinst':@;  \
+    @[\
+      - none: @[don't@ mark@ any@ symbol@ automatically@]@\n\
+      - goal: @[mark@ every@ monomorphic@ instance@ in@ the@ goal@]@\n\
+      - all:  @[mark@ every@ monomorphic@ instance@ in@ the@ task.@]\
+    @]"
 
 module OHTy = OrderedHashed(struct
   type t = ty
@@ -298,6 +293,5 @@ let discriminate env = Trans.seq [
 ]
 
 let () = Trans.register_env_transform "discriminate" discriminate
-  ~desc:"Discriminate@ polymorphic@ function@ and@ predicate@ symbols.@ \
-         Allow@ to@ keep@ some@ instantiations@ from@ being@ touched@ by@ \
-         following@ polymorphism@ encodings."
+  ~desc:"Generate@ monomorphic@ type@ instances@ of@ function@ and@ \
+         predicate@ symbols@ and@ monomorphize@ task@ premises."

src/transform/eliminate_algebraic.ml

@@ -22,6 +22,7 @@ open Task
 let meta_infinite = register_meta "infinite_type" [MTtysymbol]
   ~desc:"Specify@ that@ the@ given@ type@ has@ always@ an@ infinite@ \
          cardinality."
+
 let meta_material = register_meta "material_type_arg" [MTtysymbol;MTint]
   ~desc:"If@ the@ given@ type@ argument@ is@ instantiated@ by@ an@ infinite@ \
          type@ then@ the@ associated@ type@ constructor@ is@ infinite"
@@ -267,9 +268,9 @@ let add_indexer acc ts ty = function
 let meta_proj =
   (* projection symbol, constructor symbol, position, defining axiom *)
   register_meta "algtype projection" [MTlsymbol;MTlsymbol;MTint;MTprsymbol]
-    ~desc:"Specifies@ which@ projection@ symbol@ is@ used@ for@ the@ \
+    ~desc:"Specify@ which@ projection@ symbol@ is@ used@ for@ the@ \
            given@ constructor@ at@ the@ specified@ position.@ \
-           Internally@ used."
+           For@ internal@ use."
 
 let add_projections (state,task) _ts _ty csl =
   (* declare and define the projection functions *)
@@ -434,7 +435,7 @@ let eliminate_match =
   Trans.compose compile_match (Trans.fold_map comp empty_state init_task)
 
 let meta_elim = register_meta "eliminate_algebraic" [MTstring]
-  ~desc:"@[<hov 2>configure the 'eliminate_algebraic' transformation:@\n\
+  ~desc:"@[<hov 2>Configure the 'eliminate_algebraic' transformation:@\n\
     \"keep_types\" : @[keep algebraic type definitions@]@\n\
     \"keep_enums\" : @[keep monomorphic enumeration types@]@\n\
     \"keep_recs\"  : @[keep non-recursive records@]@\n\
@@ -492,11 +493,11 @@ let eliminate_projections = Trans.decl elim None
 
 let () =
   Trans.register_transform "compile_match" compile_match
-    ~desc:"Transform@ pattern-matching@ with@ nested@ pattern@ \
+    ~desc:"Transform@ pattern-matching@ with@ nested@ patterns@ \
       into@ nested@ pattern-matching@ with@ flat@ patterns.";
   Trans.register_transform "eliminate_match" eliminate_match
-    ~desc:"TODO";
+    ~desc:"Eliminate@ all@ pattern-matching@ expressions.";
   Trans.register_transform "eliminate_algebraic" eliminate_algebraic
     ~desc:"Replace@ algebraic@ data@ types@ by@ first-order@ definitions.";
   Trans.register_transform "eliminate_projections" eliminate_projections
-    ~desc:"TODO"
+    ~desc:"Define@ algebraic@ projection@ symbols@ separately."

src/transform/eliminate_definition.ml

@@ -48,9 +48,9 @@ let eliminate_builtin =
     Trans.decl (elim_abstract undef_ls rem_pr rem_ls rem_ts) None))))
 
 let () = Trans.register_transform "eliminate_builtin" eliminate_builtin
-  ~desc:"Eliminate@ symbols@ and@ propositions@ that@ are@ builtin@ \
-    in@ the@ prover@ (see@ 'syntax'@ and@ 'remove'@ clauses@ in@ \
-    the@ prover's@ driver)."
+  ~desc:"Eliminate@ propositions@ and@ definitions@ of@ symbols@ \
+    that@ are@ builtin@ in@ the@ prover@ (see@ 'syntax'@ and@ \
+    'remove'@ clauses@ in@ the@ prover's@ driver)."
 
 (** compute the meta_remove_* given two task one included in the other *)
 let compute_diff t1 t2 =
@@ -147,26 +147,25 @@ let eliminate_mutual_recursion = Trans.decl elim_mutual None
 let () =
   Trans.register_transform "eliminate_definition_func"
     eliminate_definition_func
-    ~desc:"Transform@ function@ definition@ into@ axioms.";
+    ~desc:"Transform@ function@ definitions@ into@ axioms.";
   Trans.register_transform "eliminate_definition_pred"
     eliminate_definition_pred
-    ~desc:"Transform@ predicate@ definition@ into@ axioms.";
+    ~desc:"Transform@ predicate@ definitions@ into@ axioms.";
   Trans.register_transform "eliminate_definition"
     eliminate_definition
-    ~desc:"Same@ as@ eliminate_definition_func/_pred@ at@ the@ same@ time.";
+    ~desc:"Transform@ function@ and@ predicate@ definitions@ into@ axioms.";
   Trans.register_transform "eliminate_recursion"
     eliminate_recursion
     ~desc:"Same@ as@ eliminate_definition,@ but@ only@ for@ recursive@ \
-           definition";
+           definitions.";
   Trans.register_transform "eliminate_non_struct_recursion"
     eliminate_non_struct_recursion
-    ~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ non@ structural@ \
-           recursive@ definition";
+    ~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ non-structural@ \
+           recursive@ definitions.";
   Trans.register_transform "eliminate_mutual_recursion"
     eliminate_mutual_recursion
-    ~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ mutual@ \
-           recursive@ definition (at@ least@ two@ functions@ or@ \
-           predicates@ defined@ at@ the@ same@ time)";
+    ~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ mutually@ \
+           recursive@ definitions."
 
 (** Bisect *)
 open Task

src/transform/eliminate_if.ml

@@ -105,12 +105,9 @@ let eliminate_if = Trans.compose eliminate_if_term eliminate_if_fmla
 
 let () =
   Trans.register_transform "eliminate_if_term" eliminate_if_term
-  ~desc:"Replaces@ terms@ of@ the@ form@ [if formula then t2 else t3]@ by@ \
-         lifting@ them@ at@ the@ level@ of@ formulas.@ This@ may@ introduce@ \
-         [if then else]@ in@ formulas.";
+    ~desc:"Replaces@ terms@ of@ the@ form@ [if f1 then t2 else t3]@ by@ \
+           lifting@ them@ at@ the@ level@ of@ formulas.";
   Trans.register_transform "eliminate_if_fmla" eliminate_if_fmla
-    ~desc:"Replaces@ formulas@ of@ the@ form@ [if f1 then f2\
-           else f3]@ by@ an@ equivalent@ formula@ using@ implications@ and@ \
-           other@ connectives.";
+    ~desc:"Eliminate@ formulas@ of@ the@ form@ [if f1 then f2 else f3].";
   Trans.register_transform "eliminate_if" eliminate_if
-    ~desc:"Apply@ both@ eliminate_if_term/fmla."
+    ~desc:"Eliminate@ all@ if-expressions."

src/transform/eliminate_inductive.ml

@@ -52,5 +52,5 @@ let elim d = match d.d_node with
 let eliminate_inductive = Trans.decl elim None
 
 let () = Trans.register_transform "eliminate_inductive" eliminate_inductive
-  ~desc:"replaces@ inductive@ predicates@ by@ (incomplete)@ axiomatic@ \
-         definitions,@ ie@ construction@ axioms@ and@ an@ inversion@ axiom."
+  ~desc:"Replace@ inductive@ predicates@ by@ (incomplete)@ axiomatic@ \
+         definitions,@ i.e.@ construction@ axioms@ and@ an@ inversion@ axiom."

src/transform/eliminate_let.ml

@@ -29,9 +29,8 @@ let eliminate_let      = Trans.rewrite (elim_t true true  Mvs.empty) None
 
 let () =
   Trans.register_transform "eliminate_let_term" eliminate_let_term
-    ~desc:"Eliminates@ let@ by@ substitution,@ at@ the@ term@ level.";
+    ~desc:"Eliminate@ let-expressions@ in@ terms.";
   Trans.register_transform "eliminate_let_fmla" eliminate_let_fmla
-    ~desc:"Eliminates@ let@ by@ substitution,@ at@ the@ predicate@ level.";
+    ~desc:"Eliminate@ let-expressions@ in@ formulas.";
   Trans.register_transform "eliminate_let" eliminate_let
-    ~desc:"Apply@ both@ eliminate_let_term/fmla"
-
+    ~desc:"Eliminate@ all@ let-expressions.";

src/transform/encoding.ml

@@ -16,35 +16,30 @@ open Task
 open Trans
 
 let meta_select_kept = register_meta_excl "select_kept" [MTstring]
-  ~desc:"@[Specify@ how@ to@ automatically@ choose@ the@ type@ that@ are@ \
-           kept@ (mark@ by@ 'encoding : kept')@ by@ the@ polymorphic@ \
-           encoding:@]@\n  \
-@[\
-  - none:@[ don't@ mark@ automatically@]@\n\
-  - goal:@[ mark@ all@ the@ closed@ type@ that@ appear@ has@ argument@ \
-            in@ the@ goal@]@\n\
-  - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\
-@]"
-let meta_enco_kept   = register_meta_excl "enco_kept"   [MTstring]
-  ~desc:"@[Specify@ how@ to@ keep@ type:@]@\n  \
-@[\
-  - @[<hov 2>twin: use@ conversion@ function@ between@ the@ kept@ types@ \
-              and@ the@ universal@ type (a complete encoding)@]@\n\
-  - @[<hov 2>instantiate: instantiate all the axioms with the kept types@]@\n\
-  - @[<hov 2>instantiate_complete: same@ as@ instantiate@ but@ keep@ a@ \
-    version@ not@ instantiated(a@ complete@ encoding).@]\
-@]"
+  ~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding : kept':@;  \
+    @[\
+      - none: @[don't@ mark@ any@ type@ automatically@]@\n\
+      - goal: @[mark@ every@ closed@ type@ in@ the@ goal@]@\n\
+      - all:  @[mark@ every@ closed@ type@ in@ the@ task.@]\
+    @]"
+
+let meta_enco_kept = register_meta_excl "enco_kept" [MTstring]
+  ~desc:"Specify@ the@ type@ protection@ transformation:@;  \
+    @[\
+      - @[<hov 2>twin: use@ conversion@ functions@ between@ the@ kept@ types@ \
+            and@ the@ universal@ type@]@\n\
+      - @[<hov 2>instantiate: instantiate the axioms with the kept types@ \
+            and@ throw@ out@ polymorphic@ formulas@ (incomplete).@]@\n\
+      - @[<hov 2>instantiate_complete: same@ as@ 'instantiate'@ but@ keep@ \
+            polymorphic@ formulas.@]\
+    @]"
+
 let meta_enco_poly   = register_meta_excl "enco_poly"   [MTstring]
-  ~desc:"@[Specify@ how@ to@ keep@ encode@ polymorphism:@]@\n  \
-@[\
-  - @[<hov 2>decoexp: TODO @]@\n\
-  - @[<hov 2>decorate: add@ around@ all@ the@ terms@ a@ function@ which@ \
-             give@ the@ type@ of@ the@ terms@]@\n\
-  - @[<hov 2>guard: add@ guards@ (hypothesis)@ in@ all@ the@ axioms@ about@ \
-             the@ type@ of@ the@ variables@]@\n\
-  - @[<hov 2>explicit: add@ type@ argument@ to@ all@ the@ polymorphic@ \
-             functions@]\
-@]"
+  ~desc:"Specify@ the@ type@ encoding@ transformation:@;  \
+    @[\
+      - @[<hov 2>decorate: put@ type@ annotations@ on@ top@ of@ terms@]@\n\
+      - @[<hov 2>guard: add@ type@ conditions@ under@ quantifiers.@]\
+    @]"
 
 let def_enco_select_smt  = "none"
 let def_enco_kept_smt    = "twin"
@@ -83,7 +78,7 @@ let encoding_tptp env = Trans.seq [
   Protect_finite.protect_finite]
 
 let () = register_env_transform "encoding_smt" encoding_smt
-  ~desc:"encode@ polymorphism@ for@ provers@ with@ sorts"
+  ~desc:"Encode@ polymorphic@ types@ for@ provers@ with@ sorts."
 
 let () = register_env_transform "encoding_tptp" encoding_tptp
-  ~desc:"encode@ polymorphism@ for@ provers@ without@ sorts"
+  ~desc:"Encode@ polymorphic@ types@ for@ provers@ without@ sorts."

src/transform/encoding_sort.ml

@@ -172,5 +172,4 @@ let t =
   Trans.fold (fold tenv) None
 
 let () = Trans.register_transform "encoding_sort" t
-  ~desc:"Remove@ each@ type@ application@ by@ discriminating@ it@ into@ one@ \
-         specific@ constant@ type."
+  ~desc:"Replace@ every@ closed@ type@ by@ a@ separate@ type@ constant."

src/transform/filter_trigger.ml

@@ -36,7 +36,7 @@ let remove_triggers =
     Trans.rewriteTF rt rf None
 
 let () = Trans.register_transform "remove_triggers" remove_triggers
-  ~desc:"Remove@ all@ the@ triggers@ from@ quantifiers."
+  ~desc:"Remove@ all@ triggers@ from@ quantifiers."
 
 let keep_no_predicate e = e.t_ty <> None
 
@@ -46,7 +46,7 @@ let filter_trigger_no_predicate =
 
 let () = Trans.register_transform "filter_trigger_no_predicate"
   filter_trigger_no_predicate
-  ~desc:"Keep@ only@ triggers@ which@ patterns@ are@ terms."
+  ~desc:"Remove@ all@ formula@ triggers@ from@ quantifiers."
 
 let keep_no_fmla = function
   | { t_ty = Some _ } -> true
@@ -58,9 +58,8 @@ let filter_trigger =
     Trans.rewriteTF rt rf None
 
 let () = Trans.register_transform "filter_trigger" filter_trigger
-  ~desc:"Same@ as@ filter_trigger_no_predicate@ but@ keep@ also@ pattern@ \
-         that@ are@ a@ predicate@ application@ (except@ equality)."
-
+  ~desc:"Remove@ all@ complex@ formula@ triggers@ \
+         (anything@ but@ predicate@ applications)."
 
 let keep_no_builtin rem_ls = function
   | { t_ty = Some _ } -> true
@@ -75,5 +74,5 @@ let filter_trigger_builtin =
 
 let () = Trans.register_transform "filter_trigger_builtin"
   filter_trigger_builtin
-  ~desc:"Same@ as@ filter_trigger_no_predicate@ but@ keep@ also@ pattern@ \
-         that@ are@ a@ predicate@ application@ not@ builtin."
+  ~desc:"Remove@ all@ complex@ or@ interpreted@ formula@ triggers@ \
+         (anything@ but@ non-built-in@ predicate@ applications)."

src/transform/induction.ml

@@ -82,15 +82,7 @@ module Svsl = Mvsl.Set
 (* DEBUGGING AND PRINTING *)
 
 let debug = Debug.register_info_flag "induction"
-  ~desc:"About@ the@ transformation@ of@ the@ goal@ using@ induction."
-
-let debug_verbose = Debug.register_info_flag "induction-verbose"
-  ~desc:"Same@ as@ induction, but@ print@ also@ the@ variables, the@ \
-         heuristics@ and@ the lexicographic@ order@ used."
-
-let debug_int = Debug.register_info_flag "induction_int_lex"
-  ~desc:"About@ the@ transformation@ of@ the@ goal@ using@ induction@ on@ \
-         the@ tuples@ of@ integers."
+  ~desc:"Print@ debugging@ messages@ of@ the@ 'induction'@ transformation."
 
 let print_ty_skm skm =
   List.iter
@@ -336,7 +328,7 @@ let induction_ty_lex km t0 =
     let lexl, rightmost_qvl = qsplit km vl qvl in
     let tcase = make_induction_lex lexl rightmost_qvl t in
 
-    if Debug.test_flag debug_verbose then
+    if Debug.test_flag debug then
       begin
 	print_vset vset;
 	print_heuristic_lex vl;
@@ -344,11 +336,6 @@ let induction_ty_lex km t0 =
 	Format.printf "Old Task: %a \n@." Pretty.print_term t0;
 	Format.printf "New Task: %a \n@." Pretty.print_term tcase
       end;
-    if Debug.test_flag debug then
-      begin
-	Format.printf "Old Task: %a \n@." Pretty.print_term t0;
-	Format.printf "New Task: %a \n@." Pretty.print_term tcase
-      end;
     [tcase]
   with No_candidates_found -> Format.printf "No candidates found\n"; [t0]
 
@@ -362,7 +349,7 @@ let induction_ty_lex = function
 
 let () =
   Trans.register_transform_l "induction_ty_lex" (Trans.store induction_ty_lex)
-    ~desc:"TODO: induction on type with lexicographic order"
+    ~desc:"Generate@ induction@ hypotheses@ for@ goals@ over@ algebraic@ types."
 
 
 (***************************************************************************)
@@ -460,7 +447,7 @@ let induction_int_lex _km (le_int,lt_int) t0 =
     begin
       let t = int_strong_induction_lex (le_int,lt_int) ivl genl t in
       let t = t_forall_close lvl [] t in
-      if Debug.test_flag debug_int then
+      if Debug.test_flag debug then
 	(Format.printf "Old Task: %a \n@." Pretty.print_term t0;
 	 Format.printf "New Task: %a \n@." Pretty.print_term t);
       [t]
@@ -485,9 +472,7 @@ let () =
     (fun env ->
       let th_int = Env.find_theory env ["int"] "Int" in
       Trans.store (induction_int_lex th_int))
-    ~desc:"TODO: induction on integers"
-
-
+    ~desc:"Generate@ induction@ hypotheses@ for@ goals@ over@ integers."
 
 (*
 Local Variables:

src/transform/inlining.ml

@@ -78,7 +78,7 @@ let fold in_goal notdeft notdeff notls task_hd (env, task) =
 (* transformations *)
 
 let meta = Theory.register_meta "inline : no" [Theory.MTlsymbol]
-  ~desc:"Disallow@ the@ inlining@ of@ the@ given@ logic@ symbols."
+  ~desc:"Disallow@ the@ inlining@ of@ the@ given@ function/predicate@ symbol."
 
 let t ?(use_meta=true) ?(in_goal=false) ~notdeft ~notdeff ~notls =
   let trans notls =
@@ -121,7 +121,7 @@ let () =
   Trans.register_transform "inline_all" all
     ~desc:"Inline@ non-recursive@ definitions.";
   Trans.register_transform "inline_goal" goal
-    ~desc:"Same@ as@ inline_all, but@ only@ inline in@ goals.";
+    ~desc:"Same@ as@ 'inline_all', but@ only@ inline in@ goals.";
   Trans.register_transform "inline_trivial" trivial
     ~desc:"Inline@ trivial@ definitions@ like@ @[f(x,y) = g(y,x,0)@]."
 

src/transform/instantiate_predicate.ml

@@ -70,5 +70,5 @@ let () =
   Trans.register_transform "instantiate_predicate"
     (Trans.on_tagged_pr meta (fun spr ->
       Trans.fold_map (trans spr) ([], Sterm.empty) None))
-    ~desc:"Look@ into@ all@ the@ task@ for@ terms@ that@ can@ instantiate@ \
-           proposition@ marked@ by@ the@ 'instantiate : auto'@ meta."
+    ~desc:"Instantiate@ proposition@ marked@ by@ 'instantiate : auto'.@ \
+           Used@ for@ Gappa."

src/transform/introduction.ml

@@ -60,6 +60,7 @@ let intros pr f =
 let () = Trans.register_transform "introduce_premises" (Trans.goal intros)
   ~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \
          goal@ into@ constant@ symbol@ and@ axioms."
+
 (*
 Local Variables:
 compile-command: "unset LANG; make -C ../.. byte"

src/transform/libencoding.ml

@@ -16,11 +16,11 @@ open Decl
 open Theory
 
 let debug = Debug.register_info_flag "encoding"
-  ~desc:"About the encoding of polymorphism."
+  ~desc:"Print@ debugging@ messages@ about@ polymorphism@ encoding."
 
 (* meta to tag the protected types *)
 let meta_kept = register_meta "encoding : kept" [MTty]
-  ~desc:"Specify a type to keep during the encoding of polymorphism."
+  ~desc:"Specify@ a@ type@ to@ keep@ during@ polymorphism@ encoding."
 
 (* sort symbol of the "universal" type *)
 let ts_base = create_tysymbol (id_fresh "uni") [] None

src/transform/lift_epsilon.ml

@@ -57,7 +57,13 @@ let lift kind =
 let lift_epsilon kind = Trans.fold (lift kind) None
 
 let meta_epsilon = Theory.register_meta_excl "lift_epsilon" [MTstring]
-  ~desc:"TODO"
+  ~desc:"Specify@ whether@ the@ existence@ of@ a@ witness@ for@ the@ \
+    formula@ under@ epsilon@ is@ assumed:@;  \
+    @[\
+      - @[<hov 2>implicit:@ implicitly@ assume@ existence@]@\n\
+      - @[<hov 2>implied:@ @ do@ not@ assume@ the@ existence@ \
+          of@ a@ witness.@]\
+    @]"
 
 let lift_epsilon = Trans.on_meta_excl meta_epsilon
   (fun alo ->
@@ -69,4 +75,4 @@ let lift_epsilon = Trans.on_meta_excl meta_epsilon
     lift_epsilon kind)
 
 let () = Trans.register_transform "lift_epsilon" lift_epsilon
-  ~desc:"TODO"
+  ~desc:"Move@ epsilon-terms@ into@ separate@ function@ definitions."

src/transform/simplify_array.ml

@@ -41,6 +41,5 @@ let make_rt_rf env =
 let t env = let rt,rf = make_rt_rf env in Trans.rewriteTF rt rf None
 
 let () = Trans.register_env_transform "simplify_array" t
-  ~desc:"Rewrite@ using@ the@ axiom@ Select_eq@ of@ theory@ map.Map@ \
-         whenever@ possible@ using@ syntaxic@ equality@ modulo@ alpha@ \
-         equivalence."
+  ~desc:"Apply,@ wherever@ possible,@ the@ axiom@ 'Select_eq'@ of@ \
+         the@ library@ theory@ map.Map."

src/transform/simplify_formula.ml

@@ -37,7 +37,7 @@ let () = Trans.register_transform
 let () = Trans.register_transform_l
   "simplify_formula_and_task" simplify_formula_and_task
   ~desc:"Same as simplify_formula, but also@ \
-         removes@ axioms@ and@ goals@ that@ become@ trivial."
+         remove@ axioms@ and@ goals@ that@ become@ trivial."