From 675dbaf2634bfd21043484e97918ab537a563e86 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 19 Mar 2019 11:38:16 +0000
Subject: 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.

---
 src/ast_util.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src')

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
-- 
cgit v1.2.3