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, 12 insertions, 1 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 8b4865594..08354ef55 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -307,6 +307,17 @@ let rename_hyp id1 id2 sign =
     (fun (_,b,t) _ -> (id2,b,t))
     (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
 
+(**********************************************************************)
+
+let name_prop_vars env sigma ctxt =
+  List.map2 (fun (na,b,t as d) s ->
+    if na = Anonymous && s = prop_sort then
+      let s = match Namegen.head_name t with Some id -> string_of_id id | None -> "" in
+      (Name (add_suffix (id_of_string "H") s),b,t)
+    else
+      d)
+    ctxt (sorts_of_context env sigma ctxt)
+
 (************************************************************************)
 (************************************************************************)
 (* Implementation of the logical rules *)
@@ -511,7 +522,7 @@ and mk_casegoals sigma goal goalacc p c =
     try Tacred.find_hnf_rectype env sigma ct
     with Not_found -> anomaly (Pp.str "mk_casegoals") in
   let (lbrty,conclty) =
-    type_case_branches_with_names env indspec p c in
+    type_case_branches_with_names (name_prop_vars env sigma) env indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')