From 4ae6a5f9f0816cf6e89fd96fb7499302f373d587 Mon Sep 17 00:00:00 2001
From: Avi Shinnar <shinnar@us.ibm.com>
Date: Wed, 10 Jan 2018 15:36:34 -0500
Subject: [PATCH] Only emit one definition/lookup of the free
 variables/constants in nnrc->js #80

---
 coq/Translation/NNRCtoJavaScript.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq/Translation/NNRCtoJavaScript.v b/coq/Translation/NNRCtoJavaScript.v
index 7308b6ded..8dada6d85 100644
--- a/coq/Translation/NNRCtoJavaScript.v
+++ b/coq/Translation/NNRCtoJavaScript.v
@@ -393,7 +393,7 @@ Section NNRCtoJavaScript.
     (* Free variables are assumed to be constant lookups *)
     (* Java equivalent: JavaScriptBackend.closeFreeVars *)
     Definition closeFreeVars (input:string) (e:nnrc) (params:list string) : nnrc :=
-      let all_free_vars := nnrc_global_vars e in
+      let all_free_vars := bdistinct (nnrc_global_vars e) in
       let wrap_one_free_var (e':nnrc) (fv:string) : nnrc :=
           if (in_dec string_dec fv params)
           then e'