Use of "H"-based names for propositional hypotheses obtained by

destruction of schemes in Type such as sumbool.

Added an option "Set Standard Proposition Elimination Names" for
governing this strategy (activated by default).

This provides names supposingly more uniform than before for those who
like to have names automatically generated, at least in the first
phase of the development process of proofs.

Examples:

*** Non dependent case ***

Goal {True}+{False}-> True.
intros [|].

Before:

  t : True
  ============================
   True

and

  f : False
  ============================
   True

After:

  H : True
  ============================
   True

  H : False
  ============================
   True

*** Dependent case ***

Goal forall x:{True}+{False}, x=x.
intros [|].

Before:

  t : True
  ============================
   left t = left t

  f : False
  ============================
   right f = right f

After:

  HTrue : True
  ============================
   left HTrue = left HTrue

  HFalse : False
  ============================
   right HFalse = right HFalse

1 files changed, 2 insertions, 2 deletions

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index fca0c64bf..1efc29c8f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -129,8 +129,8 @@ val arity_of_case_predicate :
   env -> inductive_family -> bool -> sorts -> types
 
 val type_case_branches_with_names :
-  env -> pinductive * constr list -> constr -> constr ->
-    types array * types
+  (rel_context -> rel_context) -> env -> pinductive * constr list -> constr ->
+    constr -> types array * types
 
 (** Annotation for cases *)
 val make_case_info : env -> inductive -> case_style -> case_info