From f5eb06f0d2b28fe72db12fb57458b961b9ae9d85 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 28 Dec 2008 19:03:04 +0000 Subject: - Another bug in get_sort_family_of (sort-polymorphism of constants and inductive types was not taken into account). - Virtually extended tauto to - support arbitrary-length disjunctions and conjunctions, - support arbitrary complex forms of disjunctions and conjunctions when in the contravariant of an implicative hypothesis, - stick with the purely propositional fragment and not apply reflexivity. This is virtual in the sense that it is not activated since it breaks compatibility with the existing tauto. - Modified the notion of conjunction and unit type used in hipattern in a way that is closer to the intuitive meaning (forbid dependencies between parameters in conjunction; forbid indices in unit types). - Investigated how far "iff" could be turned into a direct inductive definition; modified tauto.ml4 so that it works with the current and the alternative definition. - Fixed a bug in the error message from lookup_eliminator. - Other minor changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/indrec.ml | 3 ++- pretyping/retyping.ml | 5 ++++- 2 files changed, 6 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 996c00ebaf..689257c3b5 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -591,7 +591,8 @@ let lookup_eliminator ind_sp s = errorlabstrm "default_elim" (strbrk "Cannot find the elimination combinator " ++ pr_id id ++ strbrk ", the elimination of the inductive definition " ++ - pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++ + pr_global_env Idset.empty (IndRef ind_sp) ++ + strbrk " on sort " ++ pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 123ff43e7b..532c258fa1 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -115,8 +115,11 @@ let retype sigma metamap = 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) when isGlobalRef f -> + let t = type_of_global_reference_knowing_parameters env f args in + family_of_sort (sort_of_atomic_type env sigma t args) | App(f,args) -> - family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) + family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> anomaly "sort_of: Not a type (1)" | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) -- cgit v1.2.3