diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 16:17:09 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 16:17:09 +0000 |
| commit | f8394a52346bf1e6f98e7161e75fb65bd0631391 (patch) | |
| tree | ae133cc5207283e8c5a89bb860435b37cbf6ecdb /pretyping/matching.ml | |
| parent | 6dae53d279afe2b8dcfc43dd2aded9431944c5c8 (diff) | |
Moving Utils.list_* to a proper CList module, which includes stdlib
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/matching.ml')
| -rw-r--r-- | pretyping/matching.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index bc9c832ae..37cbcc062 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -110,7 +110,7 @@ let dummy_constr = mkProp let rec make_renaming ids = function | (Name id,Name _,_)::stk -> let renaming = make_renaming ids stk in - (try mkRel (list_index id ids) :: renaming + (try mkRel (List.index id ids) :: renaming with Not_found -> dummy_constr :: renaming) | (_,_,_)::stk -> dummy_constr :: make_renaming ids stk @@ -152,7 +152,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | _ -> error "Only bound indices allowed in second order pattern matching.") args in let frels = Intset.elements (free_rels cT) in - if list_subset frels relargs then + if List.subset frels relargs then constrain (n,([],build_lambda relargs stk cT)) subst else raise PatternMatchingFailure |