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, 10 insertions, 0 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 0c2bad5c6..53c2603d8 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)