diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 21:29:41 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 21:29:41 +0000 |
| commit | 6da011a8677676462b24940a6171fb22615c3fbb (patch) | |
| tree | 0df385cc8b8d72b3465d7745d2b97283245c7ed5 /pretyping/typing.ml | |
| parent | 133a2143413a723d1d4e3dead5ffa8458f61afa8 (diff) | |
More monomorphic List.mem + List.assoc + ...
To reduce the amount of syntactic noise, we now provide
a few inner modules Int.List, Id.List, String.List, Sorts.List
which contain some monomorphic (or semi-monomorphic) functions
such as mem, assoc, ...
NB: for Int.List.mem and co we reuse List.memq and so on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 9fe95a119..bbcc5727b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -79,8 +79,8 @@ let e_check_branch_types env evdref ind cj (lfj,explft) = done let max_sort l = - if List.mem InType l then InType else - if List.mem InSet l then InSet else InProp + if Sorts.List.mem InType l then InType else + if Sorts.List.mem InSet l then InSet else InProp let e_is_correct_arity env evdref c pj ind specif params = let arsign = make_arity_signature env true (make_ind_family (ind,params)) in @@ -93,7 +93,8 @@ let e_is_correct_arity env evdref c pj ind specif params = if not (Evarconv.e_cumul env evdref a1 a1') then error (); srec (push_rel (na1,None,a1) env) t ar' | Sort s, [] -> - if not (List.mem (family_of_sort s) allowed_sorts) then error () + if not (Sorts.List.mem (Sorts.family s) allowed_sorts) + then error () | Evar (ev,_), [] -> let s = Termops.new_sort_in_family (max_sort allowed_sorts) in evdref := Evd.define ev (mkSort s) !evdref |