diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-26 20:26:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-26 20:26:44 +0000 |
| commit | d6615c44439319e99615474cef465d25422a070d (patch) | |
| tree | f364422e44d5e40b0e649d7a03290d50b31cc5c8 /pretyping | |
| parent | c8a8c52d313bfddf27660e0de2d7ffbf4658b87c (diff) | |
- Extracted from the tactic "now" an experimental tactic "easy" for small
automation.
- Permitted to use evars in the intermediate steps of "apply in" (as expected
in the test file apply.v).
- Back on the systematic use of eq_rect (r11697) for implementing
rewriting (some proofs, especially lemma DistOoVv in
Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in
Sophia-Antipolis/Semantics/example2.v are explicitly refering
to the name of the lemmas used for rewriting).
- Fixed at the same time a bug in get_sort_of (predicativity of Set was not
taken into account).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11717 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/retyping.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 03afe0a17..123ff43e7 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -111,7 +111,10 @@ let retype sigma metamap = | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) | Sort (Prop c) -> InType | Sort (Type u) -> InType - | Prod (name,t,c2) -> sort_family_of (push_rel (name,None,t) env) c2 + | Prod (name,t,c2) -> + let s2 = sort_family_of (push_rel (name,None,t) env) c2 in + if Environ.engagement env <> Some ImpredicativeSet && + s2 = InSet & sort_family_of env t = InType then InType else s2 | App(f,args) -> family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> |