A new step in the new "standard" naming policy for propositional hypotheses

obtained from case analysis or induction. Made it under experimental status.

This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was
acting at the level of logic.ml. Now acting in tactics.ml.

Parts of things to be done about naming (not related to Propositions):
induction on H:nat+bool produces hypotheses n and b but destruct on H
produces a and b. This is because induction takes the dependent scheme
whose names are statically inferred to be a and b while destruct
dynamically builds a new scheme.

4 files changed, 33 insertions, 27 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index f6ca611a3..5e853784e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -446,21 +446,6 @@ 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 false
-
-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
@@ -489,9 +474,6 @@ let is_predicate_explicitly_dep env pred arsign =
           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
@@ -505,13 +487,11 @@ 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 preprocess_names env n brty =
+let set_names env n brty =
   let (ctxt,cl) = decompose_prod_n_assum n brty in
-  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 preprocess_names env ind brv =
+let set_pattern_names env ind brv =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let arities =
     Array.map
@@ -519,9 +499,9 @@ let set_pattern_names preprocess_names env ind brv =
         rel_context_length ((prod_assum c)) -
         mib.mind_nparams)
       mip.mind_nf_lc in
-  Array.map2 (set_names preprocess_names env) arities brv
+  Array.map2 (set_names env) arities brv
 
-let type_case_branches_with_names preprocess_names env indspec p c =
+let type_case_branches_with_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
@@ -531,7 +511,7 @@ let type_case_branches_with_names preprocess_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 preprocess_names env (fst ind) lbrty, conclty)
+    (set_pattern_names env (fst ind) lbrty, conclty)
   else (lbrty, conclty)
 
 (* Type of Case predicates *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 5583eff4d..1561cf97b 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -156,8 +156,7 @@ val arity_of_case_predicate :
   env -> inductive_family -> bool -> sorts -> types
 
 val type_case_branches_with_names :
-  (rel_context -> rel_context) -> env -> pinductive * constr list -> constr ->
-    constr -> types array * types
+  env -> pinductive * constr list -> constr -> constr -> types array * types
 
 (** Annotation for cases *)
 val make_case_info : env -> inductive -> case_style -> case_info
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 8b9e6e633..16ba03ad7 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -367,3 +367,25 @@ let rename_bound_vars_as_displayed avoid env c =
     | _ -> c
   in
   rename avoid env c
+
+(**********************************************************************)
+(* "H"-based naming strategy introduced June 2014 for hypotheses in
+   Prop produced by case/elim/destruct/induction, in place of the
+   strategy that was using the first letter of the type, leading to
+   inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar
+   types *)
+
+let h_based_elimination_names = ref false
+
+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 }
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index cb2891996..88ce43f8e 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -95,3 +95,8 @@ val compute_displayed_let_name_in :
   renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val rename_bound_vars_as_displayed :
   Id.t list -> Name.t list -> types -> types
+
+(**********************************************************************)
+(* Naming strategy for arguments in Prop when eliminating inductive types *)
+
+val use_h_based_elimination_names : unit -> bool