diff options
| -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 1be41458d4..7c1e9aea5e 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 *) |