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.

9 files changed, 99 insertions, 58 deletions

diff --git a/CHANGES b/CHANGES
index ac76b9eca..335b793ea 100644
--- a/CHANGES
+++ b/CHANGES
@@ -657,9 +657,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").
+- New experimental option "Set Standard Proposition Elimination Names"
+  so that case analysis or induction on schemes in Type containing
+  propositions now produces "H"-based names.
 
 Tactic definitions
 
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
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e1cbe4af0..59de85901 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -314,14 +314,6 @@ let rename_hyp id1 id2 sign =
 
 (**********************************************************************)
 
-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 Namegen.default_prop_ident s),b,t)
-    else
-      d)
-    ctxt (sorts_of_context env sigma ctxt)
 
 (************************************************************************)
 (************************************************************************)
@@ -526,8 +518,7 @@ and mk_casegoals sigma goal goalacc p c =
   let indspec =
     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 (name_prop_vars env sigma) env indspec p c in
+  let (lbrty,conclty) = type_case_branches_with_names env indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')
 
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2c21f9809..a23ae4e82 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -337,7 +337,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
     Proofview.V82.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*>
       general_elim_clause with_evars frzevars tac cls c t l
       (match lft2rgt with None -> false | Some b -> b)
-      {elimindex = None; elimbody = (elim,NoBindings)}
+      {elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
   end
 
 let adjust_rewriting_direction args lft2rgt =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3b1cf6575..442f0a3cb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -829,7 +829,44 @@ let index_of_ind_arg t =
       | None -> error "Could not find inductive argument of elimination scheme."
   in aux None 0 t
 
-let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i (elim, elimty, bindings) indclause gl =
+let enforce_prop_bound_names rename tac =
+  match rename with
+  | Some (isrec,nn) when Namegen.use_h_based_elimination_names () ->
+      (* Rename dependent arguments in Prop with name "H" *)
+      (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *)
+      (* elim or induction with schemes built by Indrec.build_induction_scheme *)
+      let rec aux env sigma i t =
+        if i = 0 then t else match kind_of_term t with
+        | Prod (Name _ as na,t,t') ->
+            let very_standard = true in
+            let na =
+              if Retyping.get_sort_family_of env sigma t = InProp then
+                (* "very_standard" says that we should have "H" names only, but
+                   this would break compatibility even more... *)
+                let s = match Namegen.head_name t with
+                  | Some id when not very_standard -> string_of_id id
+                  | _ -> "" in
+                Name (add_suffix Namegen.default_prop_ident s)
+              else
+                na in
+            mkProd (na,t,aux (push_rel (na,None,t) env) sigma (i-1) t')
+        | Prod (Anonymous,t,t') ->
+            mkProd (Anonymous,t,aux (push_rel (Anonymous,None,t) env) sigma (i-1) t')
+        | LetIn (na,c,t,t') ->
+            mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t')
+        | _ -> print_int i; Pp.msg (print_constr t); assert false in
+      let rename_branch i gl =
+        let env = pf_env gl in
+        let sigma = project gl in
+        let t = pf_concl gl in
+        change_concl (aux env sigma i t) gl in
+      (if isrec then tclTHENFIRSTn else tclTHENLASTn)
+        tac
+        (Array.map rename_branch nn)
+  | _ ->
+      tac
+
+let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause gl =
   let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in
   let indmv =
     (match kind_of_term (nth_arg i elimclause.templval.rebus) with
@@ -838,7 +875,7 @@ let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i (elim, elimty,
              (str "The type of elimination clause is not well-formed."))
   in
   let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
-  Proofview.V82.of_tactic (Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags) gl
+  enforce_prop_bound_names rename (Proofview.V82.of_tactic (Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags)) gl
 
 (*
  * Elimination tactic with bindings and using an arbitrary
@@ -850,6 +887,7 @@ let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i (elim, elimty,
 
 type eliminator = {
   elimindex : int option;  (* None = find it automatically *)
+  elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
   elimbody : constr with_bindings
 }
 
@@ -858,12 +896,12 @@ let general_elim_clause_gen elimtac indclause elim gl =
   let elimt = pf_type_of gl elimc in
   let i =
     match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
-  elimtac i (elimc, elimt, lbindelimc) indclause gl
+  elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause gl
 
 let general_elim with_evars (c, lbindc) elim gl =
-  let elimtac = elimination_clause_scheme with_evars in
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
+  let elimtac = elimination_clause_scheme with_evars in
   let indclause  = pf_apply make_clenv_binding gl (c, t) lbindc in
   general_elim_clause_gen elimtac indclause elim gl
 
@@ -879,7 +917,8 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl =
       pf_apply build_case_analysis_scheme_default gl mind sort in
   tclTHEN (tclEVARS sigma)
   (general_elim with_evars (c,lbindc)
-   {elimindex = None; elimbody = (elim,NoBindings)}) gl
+   {elimindex = None; elimbody = (elim,NoBindings);
+    elimrename = Some (false, constructors_nrealdecls (fst mind))}) gl
 
 let general_case_analysis with_evars (c,lbindc as cx) =
   match kind_of_term c with
@@ -907,7 +946,8 @@ let find_eliminator c gl =
   let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_type_of gl c) in
   if is_record ind <> None then raise IsRecord;
   let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
-    evd, {elimindex = None; elimbody = (c,NoBindings)}
+    evd, {elimindex = None; elimbody = (c,NoBindings);
+          elimrename = Some (true, constructors_nrealdecls ind)}
 
 let default_elim with_evars (c,_ as cx) =
   Proofview.tclORELSE
@@ -926,7 +966,9 @@ let default_elim with_evars (c,_ as cx) =
 
 let elim_in_context with_evars c = function
   | Some elim ->
-      Proofview.V82.tactic (general_elim with_evars c {elimindex = Some (-1); elimbody = elim})
+      Proofview.V82.tactic
+        (general_elim with_evars c {elimindex = Some (-1); elimbody = elim;
+                                    elimrename = None})
   | None -> default_elim with_evars c
 
 let elim with_evars (c,lbindc as cx) elim =
@@ -957,7 +999,7 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
     (* Set the hypothesis name in the message *)
     raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
 
-let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i (elim, elimty, bindings) indclause gl =
+let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause gl =
   let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
   let hypmv =
@@ -978,9 +1020,9 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i (elim, e
   clenv_refine_in with_evars id elimclause'' gl
 
 let general_elim_clause with_evars flags id c e =
-  let elim gl = match id with
-  | None -> elimination_clause_scheme with_evars ~flags gl
-  | Some id -> elimination_in_clause_scheme with_evars ~flags id gl
+  let elim = match id with
+  | None -> elimination_clause_scheme with_evars ~flags
+  | Some id -> elimination_in_clause_scheme with_evars ~flags id
   in
   Proofview.V82.tactic (fun gl -> general_elim_clause_gen elim c e gl)
 
@@ -3052,7 +3094,7 @@ let find_induction_type isrec elim hyp0 gl =
 	let scheme = compute_elim_sig ~elimc elimt in
 	if Option.is_empty scheme.indarg then error "Cannot find induction type";
 	let indsign = compute_scheme_signature scheme hyp0 ind_guess in
-	let elim = ({elimindex = Some(-1); elimbody = elimc},elimt) in
+	let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in
 	evd, scheme, ElimUsing (elim,indsign) in
   evd,(Option.get scheme.indref,scheme.nparams, elim)
 
@@ -3077,8 +3119,9 @@ let get_eliminator elim gl = match elim with
       Proofview.Goal.sigma gl, (* bugged, should be computed *) true, elim, indsign
   | ElimOver (isrec,id) ->
       let evd, (elimc,elimt),_ as elims = guess_elim isrec id gl in
-      let _, (l, _) = compute_elim_signature elims id in
-      evd, isrec, ({elimindex = None; elimbody = elimc}, elimt), l
+      let _, (l, s) = compute_elim_signature elims id in
+      let branchlengthes = List.map (fun (_,b,c) -> assert (b=None); pi1 (decompose_prod_letin c)) (List.rev s.branches) in
+      evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l
 
 (* Instantiate all meta variables of elimclause using lid, some elts
    of lid are parameters (first ones), the other are
@@ -3219,18 +3262,18 @@ let induction_from_context_l with_evars elim_info lid names =
     (* FIXME: Tester ca avec un principe dependant et non-dependant *)
     induction_tac_felim with_evars realindvars scheme.nparams elim
   ]) in
-  let elim = ElimUsing (({elimindex = Some scheme.index; elimbody = Option.get scheme.elimc}, scheme.elimt), indsign) in
+  let elim = ElimUsing (({elimindex = Some scheme.index; elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in
   apply_induction_in_context
     None elim (hyp0::indvars) names induct_tac
 
 (* Unification between ((elimc:elimt) ?i ?j ?k ?l ... ?m) and the
    hypothesis on which the induction is made *)
 let induction_tac with_evars elim (varname,lbind) typ gl =
-  let ({elimindex=i;elimbody=(elimc,lbindelimc)},elimt) = elim in
+  let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
   let indclause = pf_apply make_clenv_binding gl (mkVar varname,typ) lbind  in
   let i = match i with None -> index_of_ind_arg elimt | Some i -> i in
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
-  elimination_clause_scheme with_evars i (elimc, elimt, lbindelimc) indclause gl
+  elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause gl
 
 let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
   inhyps =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7d88b7a90..20b974a82 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -241,6 +241,7 @@ val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme
 (** elim principle with the index of its inductive arg *)
 type eliminator = {
   elimindex : int option;  (** None = find it automatically *)
+  elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
   elimbody : constr with_bindings
 }