From 3a2de1b11a8873fbe4f3adfc2b17883a5e493bb3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 16 Dec 2003 17:26:57 +0000
Subject: Correction bug 371 (sub_match retournait des instances non closes)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5106 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/matching.ml  | 4 +++-
 pretyping/matching.mli | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index b42365679b..06fdc778ee 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -164,8 +164,10 @@ let pmatches = matches_core None true
 (* To skip to the next occurrence *)
 exception NextOccurrence of int
 
-(* Tells if it is an authorized occurrence *)
+(* Tells if it is an authorized occurrence and if the instance is closed *)
 let authorized_occ nocc mres =
+  if not (List.for_all (fun (_,c) -> closed0 c) (fst mres)) then
+    raise PatternMatchingFailure;
   if nocc = 0 then mres
   else raise (NextOccurrence nocc)
 
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 32c2906b64..c7c9905ee7 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -42,7 +42,7 @@ val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
 (* To skip to the next occurrence *)
 exception NextOccurrence of int
 
-(* Tries to match a subterm of [c] with [pat] *)
+(* Tries to match a _closed_ subterm of [c] with [pat] *)
 val sub_match : int -> constr_pattern -> constr -> patvar_map * constr
 
 (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
-- 
cgit v1.2.3