diff options
| author | barras | 2009-06-22 15:40:36 +0000 |
|---|---|---|
| committer | barras | 2009-06-22 15:40:36 +0000 |
| commit | b0a8a08682c8f9c8f3457adef403c48f8fc011ac (patch) | |
| tree | a237dc3fa9db5cbdc89ed9fd2b0ba7b386b1b860 | |
| parent | 339418b59ec90edbe16980e2978a0e8be347aa1e (diff) | |
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
| -rw-r--r-- | pretyping/evarutil.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 -> |