Commit 3a649d5c authored by charguer's avatar charguer

encours

parent bb5c9fe2
(*---------polymorphism -----------*)
let test_poly () = let x = [] in x
(*---------simple record------------*)
type 'a myrec = {
......
......@@ -36,7 +36,7 @@ let lift_ident_name id =
let name = Ident.name id in
if name = "OkaStream" then "CFPrim" else (* TODO : improve *)
if Ident.persistent id
then name ^ "_ml" (* TODO: also emit a Require directive on name ^ "_ml" *)
then (Printf.printf "require %s\n" name; name ^ "_ml")
else "ML" ^ name
let rec lift_full_path = function
......@@ -194,7 +194,7 @@ let coq_of_constructor p c =
let x = string_of_path p in
match find_builtin_constructor x with
| None -> coq_app_var_wilds x (typ_arity_constr c)
| Some y -> Coq_var y
| Some (y,arity) -> coq_app_var_wilds y arity
(*#########################################################################*)
......
......@@ -135,15 +135,15 @@ let all_primitives_table =
inductive data constructors in Coq. *)
let builtin_constructors_table =
[ "[]", "Coq.Lists.List.nil";
"::", "Coq.Lists.List.cons";
"()", "Coq.Init.Datatypes.tt";
"true", "Coq.Init.Datatypes.true";
"false", "Coq.Init.Datatypes.false";
"Nil", "Coq.Lists.List.nil";
"Cons", "Coq.Lists.List.cons";
"OkaStream.Nil", "Coq.Lists.List.nil";
"OkaStream.Cons", "Coq.Lists.List.cons";
[ "[]", ("Coq.Lists.List.nil", 1);
"::", ("Coq.Lists.List.cons", 1);
"()", ("Coq.Init.Datatypes.tt", 0);
"true", ("Coq.Init.Datatypes.true", 0);
"false", ("Coq.Init.Datatypes.false", 0);
"Nil", ("Coq.Lists.List.nil", 1);
"Cons", ("Coq.Lists.List.cons", 1);
"OkaStream.Nil", ("Coq.Lists.List.nil", 1);
"OkaStream.Cons", ("Coq.Lists.List.cons", 1);
]
(* --todo: add [Pervasives] as prefix *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment