Only emit one definition/lookup of the free variables/constants in nn…

…rc->js #80
querycert · Jan 10, 2018 · 4ae6a5f · 4ae6a5f
1 parent dff8814
commit 4ae6a5f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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'