diff options
author | 2013-10-24 21:29:41 +0000 | |
---|---|---|
committer | 2013-10-24 21:29:41 +0000 | |
commit | 6da011a8677676462b24940a6171fb22615c3fbb (patch) | |
tree | 0df385cc8b8d72b3465d7745d2b97283245c7ed5 /pretyping/indrec.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/indrec.ml')
-rw-r--r-- | pretyping/indrec.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 23996282c..bf9fd8a10 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -55,7 +55,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind = mib.mind_params_ctxt in - if not (List.mem kind (elim_sorts specif)) then + if not (Sorts.List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError (NotAllowedCaseAnalysis (false, Termops.new_sort_in_family kind, ind))); @@ -508,10 +508,10 @@ let check_arities listdepkind = let _ = List.fold_left (fun ln ((_,ni as mind),mibi,mipi,dep,kind) -> let kelim = elim_sorts (mibi,mipi) in - if not (List.exists ((==) kind) kelim) then raise + if not (Sorts.List.mem kind kelim) then raise (RecursionSchemeError (NotAllowedCaseAnalysis (true, Termops.new_sort_in_family kind,mind))) - else if List.mem ni ln then raise + else if Int.List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) else ni::ln) [] listdepkind |