diff options
| author | Thomas Bauereiss | 2018-06-25 20:12:40 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-06-25 20:12:40 +0100 |
| commit | ba73592a1718df30879d093b473cc81336ce63f3 (patch) | |
| tree | e1e0b903b6a7d107724be9b27c8ce386f2fc928d /src | |
| parent | 90f4906af7b4369d6759e5edbbf8a3aaac4d77e6 (diff) | |
Check for variables in disjointness check
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 4d850dc6..1696c727 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1071,6 +1071,8 @@ let rec disjoint_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = | _, P_typ (_, pat2) -> disjoint_pat pat1 pat2 | P_var (pat1, _), _ -> disjoint_pat pat1 pat2 | _, P_var (pat2, _) -> disjoint_pat pat1 pat2 + | P_id id, _ when id_is_unbound id (env_of_annot annot1) -> false + | _, P_id id when id_is_unbound id (env_of_annot annot2) -> false | P_id id1, P_id id2 -> Id.compare id1 id2 <> 0 | P_app (id1, args1), P_app (id2, args2) -> Id.compare id1 id2 <> 0 || List.exists2 disjoint_pat args1 args2 |