feature(*): Add simple toplevel module and BigInt literals

Signed-off-by: Jerome Simeon <jeromesimeon@me.com>

Author: jeromesimeon

.gitignore

@@ -1,5 +1,6 @@
 *.d
 *.vo
+*.vio
 *.glob
 
 TAGS

coq-jsast.opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 name: "coq-jsast"
-version: "2.0.0"
+version: "3.0.0"
 synopsis: "A minimal JavaScript syntax tree carved out of the JsCert project"
 description: """
 A minimal JavaScript syntax tree carved out of the JsCert project, with additional support for let bindings and using native floats.

coq/JsSyntax.v

@@ -1,6 +1,7 @@
 Set Implicit Arguments.
 Require Export Ascii String.
 Require JsNumber.
+Require Import ZArith.
 Notation "'number'" := (JsNumber.number).
 
 
@@ -63,7 +64,8 @@ Inductive literal :=
   | literal_null : literal
   | literal_bool : bool -> literal
   | literal_number : number -> literal
-  | literal_string : string -> literal.
+  | literal_string : string -> literal
+  | literal_bigint : Z -> literal.
 
 (** Labels literals used by break and continue keywords,
     including the special "empty" label. *)
@@ -187,3 +189,12 @@ Coercion stat_expr : expr >-> stat.
 Coercion label_string : string >-> label.
 
 
+Inductive topdecl :=
+| strictmode : topdecl                            (** strict mode declaration *)
+| comment : string -> topdecl                     (** comment *)
+| elementdecl : element -> topdecl                (** Program element *)
+| classdecl : string -> list funcdecl -> topdecl  (** Class declarations *)
+| constdecl : string -> expr -> topdecl           (** Constant declarations *)
+.
+
+Definition module := list topdecl.