diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-10 10:26:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-10 10:26:29 +0000 |
| commit | 6d5425d3f0ac6a0d78d51ba566d46e1bd50f5a20 (patch) | |
| tree | 1dd54841022287a053eb239cf131980aa18f4689 | |
| parent | ba268db78c86f9ca0ccdb2524193e5346f7155b3 (diff) | |
Protection contre les variables anonymes dans match_aconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3413 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/topconstr.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1be41458d..7c1e9aea5 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -232,7 +232,13 @@ type interpretation = (identifier * scope_name list) list * aconstr let match_aconstr c (metas_scl,pat) = let subst = match_ [] (List.map fst metas_scl) [] c pat in (* Reorder canonically the substitution *) - List.map (fun (x,scl) -> (List.assoc x subst,scl)) metas_scl + let find x subst = + try List.assoc x subst + with Not_found -> + (* Happens for binders bound to Anonymous *) + (* Find a better way to propagate Anonymous... *) + RVar (dummy_loc,x) in + List.map (fun (x,scl) -> (find x subst,scl)) metas_scl (**********************************************************************) (*s Concrete syntax for terms *) |