Correct extraction of nat, list, list2. Minor differences: 1) range values become 0. I think range values are not needed by codegen. 2) references to constants defined in the current module also have fully scoped names (Test.nnat instead of nnat). Perhaps it should be the job of the OCaml AST to OCaml code printer to deal with that issue.
Correct extraction of nat, list, list2.
Minor differences:
1) range values become 0. I think range values are not needed by codegen.
2) references to constants defined in the current module also have fully scoped names (Test.nnat instead of nnat). Perhaps it should be the job of the OCaml AST to OCaml code printer to deal with that issue.

Up next : need some fixes to properly handle indexed inductive types

(*new followed by old*)

[MLS_Ty
   [("nnat", [],
     Some (MLTD_DType [("O", []); ("S", [MLTY_Named ([],(["Test"], "nnat"))])]))];
[MLS_Ty
   [("nnat", [],
     Some (MLTD_DType [("O", []); ("S", [MLTY_Named ([],([], "nnat"))])]))];

 MLS_Ty
   [("list", [("a", 0)],
     Some
       (MLTD_DType
          [("Nil", []);
           ("Cons",
            [MLTY_Var ("a", 0);
             MLTY_Named ([MLTY_Var ("a", 0)],(["Test"], "list"))])]))];
 MLS_Ty
   [("list", [("'a", 4)],
     Some
       (MLTD_DType
          [("Nil", []);
           ("Cons",
            [MLTY_Var ("'a", 4); MLTY_Named ([MLTY_Var ("'a", 4)],([], "list"))])]))];

 MLS_Ty
   [("list2", [("'a", 0); ("b", 0)],
     Some
       (MLTD_DType
          [("Nil2", []);
           ("Cons2",
            [MLTY_Var ("'a", 0); MLTY_Var ("b", 0);
             MLTY_Named
               ([MLTY_Var ("'a", 0); MLTY_Var ("b", 0)],(["Test"], "list2"))])]))]]
MLS_Ty
   [("list2", [("'a", 5); ("'b", 6)],
     Some
       (MLTD_DType
          [("Nil2", []);
           ("Cons2",
            [MLTY_Var ("'a", 5); MLTY_Var ("'b", 6);
             MLTY_Named ([MLTY_Var ("'a", 5); MLTY_Var ("'b", 6)],([], "list2"))])]))]]

MallabaevAzamat/FStar,YaccConstructor/FStar,aa755/FStar,hoheinzollern/FStar,A-Manning/FStar,A-Manning/FStar,MallabaevAzamat/FStar,hoheinzollern/FStar,msprotz/FStar,YaccConstructor/FStar,A-Manning/FStar,FStarLang/FStar,FStarLang/FStar,YaccConstructor/FStar,YaccConstructor/FStar,FStarLang/FStar,MallabaevAzamat/FStar,MallabaevAzamat/FStar,hoheinzollern/FStar,aa755/FStar,hoheinzollern/FStar,aa755/FStar,msprotz/FStar,msprotz/FStar,msprotz/FStar,aa755/FStar