diff options
| author | Hugo Herbelin | 2014-06-01 10:26:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-01 11:33:55 +0200 |
| commit | bf7d2a3ad2535e7d57db79c17c81aaf67d956965 (patch) | |
| tree | de867d07739f84497e8460ba763a4221199b457d /pretyping/retyping.mli | |
| parent | 76adb57c72fccb4f3e416bd7f3927f4fff72178b (diff) | |
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
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 |