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

8 files changed, 80 insertions, 25 deletions

diff --git a/CHANGES b/CHANGES
index a3c8bf6f05..1847df58e6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -590,6 +590,9 @@ Other tactics
   clears (resp. reverts) H and all the hypotheses that depend on H.
 - Ltac's pattern-matching now supports matching metavariables that
   depend on variables bound upwards in the pattern.
+- Case analysis on schemes in Type containing Proposition now produces
+  "H"-based names (important source of incompatibility that can be
+  repaired by using option "Unset Standard Proposition Elimination Names").
 
 Tactic definitions
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e180c13465..07dacd0ccc 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 *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index fca0c64bf5..1efc29c8fd 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
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index c6c21f0259..0581f7283e 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -61,6 +61,20 @@ let is_constructor id =
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
+let head_name c = (* Find the head constant of a constr if any *)
+  let rec hdrec c =
+    match kind_of_term c with
+    | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
+    | Cast (c,_,_) | App (c,_) -> hdrec c
+    | Proj (kn,_) -> Some (Label.to_id (con_label kn))
+    | Const _ | Ind _ | Construct _ | Var _ ->
+	Some (basename_of_global (global_of_constr c))
+    | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
+	Some (match lna.(i) with Name id -> id | _ -> assert false)
+    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None
+  in
+  hdrec c
+
 let lowercase_first_char id = (* First character of a constr *)
   Unicode.lowercase_first_char (Id.to_string id)
 
@@ -71,11 +85,8 @@ let sort_hdchar = function
 let hdchar env c =
   let rec hdrec k c =
     match kind_of_term c with
-    | Prod (_,_,c)    -> hdrec (k+1) c
-    | Lambda (_,_,c)  -> hdrec (k+1) c
-    | LetIn (_,_,_,c) -> hdrec (k+1) c
-    | Cast (c,_,_)    -> hdrec k c
-    | App (f,l)       -> hdrec k f
+    | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
+    | Cast (c,_,_) | App (c,_) -> hdrec k c
     | Proj (kn,_)
     | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
     | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
@@ -89,13 +100,10 @@ let hdchar env c =
 	     | (Name id,_,_)   -> lowercase_first_char id
 	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
 	   with Not_found -> "y")
-    | Fix ((_,i),(lna,_,_)) ->
-	let id = match lna.(i) with Name id -> id | _ -> assert false in
-	lowercase_first_char id
-    | CoFix (i,(lna,_,_)) ->
+    | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
 	let id = match lna.(i) with Name id -> id | _ -> assert false in
 	lowercase_first_char id
-    | Meta _|Evar _|Case (_, _, _, _) -> "y"
+    | Meta _ | Evar _ | Case (_, _, _, _) -> "y"
   in
   hdrec 0 c
 
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 095c7a59fd..857867f3a9 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -19,6 +19,7 @@ val sort_hdchar : sorts -> string
 val hdchar : env -> types -> string
 val id_of_name_using_hdchar : env -> types -> Name.t -> Id.t
 val named_hd : env -> types -> Name.t -> Name.t
+val head_name : types -> Id.t option
 
 val mkProd_name : env -> Name.t * types * types -> types
 val mkLambda_name : env -> Name.t * types * constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 0c2bad5c6a..53c2603d8c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -232,3 +232,13 @@ let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
 
 (* Makes an unsafe judgment from a constr *)
 let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
+
+(* Returns sorts of a context *)
+let sorts_of_context env evc ctxt =
+  let rec aux = function
+  | [] -> env,[]
+  | (_,_,t as d)::ctxt ->
+      let env,sorts = aux ctxt in
+      let s = get_sort_of env evc t in
+      (push_rel d env,s::sorts) in
+  snd (aux ctxt)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index b8b458555a..a694faf4ed 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -8,6 +8,7 @@
 
 open Term
 open Evd
+open Context
 open Environ
 
 (** This family of functions assumes its constr argument is known to be
@@ -42,3 +43,5 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
 
 val type_of_global_reference_knowing_conclusion :
   env -> evar_map -> constr -> types -> evar_map * types
+
+val sorts_of_context : env -> evar_map -> rel_context -> sorts list
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 8b48655940..08354ef556 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')