diff options
| author | Brian Campbell | 2019-03-19 11:38:16 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-19 11:38:16 +0000 |
| commit | 675dbaf2634bfd21043484e97918ab537a563e86 (patch) | |
| tree | 2a345e3dd7f998f552ff743102c1f16de35259a9 /src | |
| parent | 4a720666bc5fb20c128e39d63f73aeb0a5cd6f0d (diff) | |
Don't expand set constraints when substituting vars for vars
It helps the Coq backend if the shape of constraints embedded in types
doesn't change too much.
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 96849f88..a7c97338 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1771,6 +1771,8 @@ and constraint_subst_aux l sv subst = function | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_set (kid, ints) as set_nc -> begin match subst with + | A_aux (A_nexp (Nexp_aux (Nexp_var kid',_)), _) when Kid.compare kid sv = 0 -> + NC_set (kid', ints) | A_aux (A_nexp n, _) when Kid.compare kid sv = 0 -> nexp_set_to_or l n ints | _ -> set_nc |