(refactor) Remove containsb, use in_dec instead

Signed-off-by: Jerome Simeon <[email protected]>
accordproject · Aug 15, 2018 · 8d8208e · 8d8208e
1 parent 8d1eb2b
commit 8d8208e
Show file tree

Hide file tree

Showing 5 changed files with 22,930 additions and 20,378 deletions.
diff --git a/mechanization/Common/Utils/Misc.v b/mechanization/Common/Utils/Misc.v
@@ -16,15 +16,6 @@ Require Import String.
 Require Import List.
 
 Section Misc.
-  Fixpoint containsb (x : string) (ls : list string) : bool :=
-    match ls with
-    | nil => false
-    | x'::ls' =>
-      if String.string_dec x x'
-      then true
-      else containsb x ls'
-    end.
-
   Definition multi_append {A} separator (f:A -> string) (elems:list A) : string :=
     match elems with
     | nil => ""

diff --git a/mechanization/Translation/ErgotoErgoC.v b/mechanization/Translation/ErgotoErgoC.v
@@ -369,7 +369,7 @@ Section ErgotoErgoC.
     | DImport prov import => esuccess (nil, ctxt)
     | DType prov ergo_type =>
       let name := ergo_type.(type_declaration_name) in
-      if containsb name (map type_declaration_name
+      if in_dec string_dec name (map type_declaration_name
                             (ctxt.(compilation_context_new_type_decls) ++
                              ctxt.(compilation_context_type_decls))) then
         efailure (ETypeError prov ("Cannot redefine type `" ++ name ++ "'"))

diff --git a/packages/ergo-cli/lib/ergoc-lib.js b/packages/ergo-cli/lib/ergoc-lib.js
diff --git a/packages/ergo-cli/lib/ergotop-lib.js b/packages/ergo-cli/lib/ergotop-lib.js
diff --git a/packages/ergo-compiler/lib/ergo-core.js b/packages/ergo-compiler/lib/ergo-core.js