summaryrefslogtreecommitdiff
path: root/pretyping/matching.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /pretyping/matching.ml
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'pretyping/matching.ml')
-rw-r--r--pretyping/matching.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index aaa4c3f0..d066a58d 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: matching.ml 10451 2008-01-18 17:20:28Z barras $ *)
+(* $Id: matching.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
(*i*)
open Util
@@ -85,7 +85,7 @@ let matches_core convert allow_partial_app pat c =
List.map
(function
| PRel n -> n
- | _ -> error "Only bound indices allowed in second order pattern matching")
+ | _ -> 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
@@ -185,7 +185,7 @@ let matches_core convert allow_partial_app pat c =
in
Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c)
-let matches = matches_core None false
+let matches = matches_core None true
let pmatches = matches_core None true