From b0a8a08682c8f9c8f3457adef403c48f8fc011ac Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 22 Jun 2009 15:40:36 +0000
Subject: documented a bug of pattern unification with metas

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12203 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8e9ddf1baf..029616e599 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1036,7 +1036,10 @@ let is_unification_pattern (env,nb) f l t =
 
 (* From a unification problem "?X l1 = term1 l2" such that l1 is made
    of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *)
-
+(* NB: does not work when (term1 l2) contains metas because metas
+   *implicitly* depend on Vars but lambda abstraction will not reflect this 
+   dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
+   return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
 let solve_pattern_eqn env l1 c =
   let l1 = List.map (expand_var env) l1 in
   let c' = List.fold_right (fun a c ->
-- 
cgit v1.2.3