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

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e180c1346..07dacd0cc 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -307,7 +307,7 @@ let make_arity_signature env dep indf =
   let (arsign,_) = get_arity env indf in
   if dep then
     (* We need names everywhere *)
-    name_context env
+    Namegen.name_context env
       ((Anonymous,None,build_dependent_inductive env indf)::arsign)
       (* Costly: would be better to name once for all at definition time *)
   else
@@ -320,7 +320,7 @@ let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s)
 let build_branch_type env dep p cs =
   let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
   if dep then
-    it_mkProd_or_LetIn_name env
+    Namegen.it_mkProd_or_LetIn_name env
       (applist (base,[build_dependent_constructor cs]))
       cs.cs_args
   else
@@ -371,13 +371,28 @@ let find_coinductive env sigma c =
 (* find appropriate names for pattern variables. Useful in the Case
    and Inversion (case_then_using et case_nodep_then_using) tactics. *)
 
+let h_based_elimination_names = ref true
+
+let use_h_based_elimination_names () =
+  !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4
+
+open Goptions
+
+let _ = declare_bool_option
+	  { optsync  = true;
+            optdepr  = false;
+	    optname  = "use of \"H\"-based proposition names in elimination tactics";
+	    optkey   = ["Standard";"Proposition";"Elimination";"Names"];
+	    optread  = (fun () -> !h_based_elimination_names);
+	    optwrite = (:=) h_based_elimination_names }
+
 let is_predicate_explicitly_dep env pred arsign =
   let rec srec env pval arsign =
     let pv' = whd_betadeltaiota env Evd.empty pval in
     match kind_of_term pv', arsign with
       | Lambda (na,t,b), (_,None,_)::arsign ->
 	  srec (push_rel_assum (na,t) env) b arsign
-      | Lambda (na,_,_), _ ->
+      | Lambda (na,_,t), _ ->
 
        (* The following code has an impact on the introduction names
 	  given by the tactics "case" and "inversion": when the
@@ -396,10 +411,12 @@ let is_predicate_explicitly_dep env pred arsign =
 	  dependency status (of course, Anonymous implies non
 	  dependent, but not conversely).
 
-          At the end, this is only to preserve the compatibility: a
-          check whether the predicate is actually dependent or not
-          would indeed be more natural! *)
+          From Coq > 8.2, using or not the the effective dependency of
+          the predicate is parametrable! *)
 
+	  if use_h_based_elimination_names () then
+	    dependent (mkRel 1) t
+	  else
           begin match na with
           | Anonymous -> false
           | Name _ -> true
@@ -413,11 +430,13 @@ let is_elim_predicate_explicitly_dependent env pred indf =
   let arsign,_ = get_arity env indf in
   is_predicate_explicitly_dep env pred arsign
 
-let set_names env n brty =
+let set_names preprocess_names env n brty =
   let (ctxt,cl) = decompose_prod_n_assum n brty in
-  it_mkProd_or_LetIn_name env cl ctxt
+  let ctxt =
+    if use_h_based_elimination_names () then preprocess_names ctxt else ctxt in
+  Namegen.it_mkProd_or_LetIn_name env cl ctxt
 
-let set_pattern_names env ind brv =
+let set_pattern_names preprocess_names env ind brv =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let arities =
     Array.map
@@ -425,9 +444,9 @@ let set_pattern_names env ind brv =
         rel_context_length ((prod_assum c)) -
         mib.mind_nparams)
       mip.mind_nf_lc in
-  Array.map2 (set_names env) arities brv
+  Array.map2 (set_names preprocess_names env) arities brv
 
-let type_case_branches_with_names env indspec p c =
+let type_case_branches_with_names preprocess_names env indspec p c =
   let (ind,args) = indspec in
   let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in
   let nparams = mib.mind_nparams in
@@ -437,7 +456,7 @@ let type_case_branches_with_names env indspec p c =
   let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env p (ind,params) then
-    (set_pattern_names env (fst ind) lbrty, conclty)
+    (set_pattern_names preprocess_names env (fst ind) lbrty, conclty)
   else (lbrty, conclty)
 
 (* Type of Case predicates *)