Commit 7209c060 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

explicit_polymorphism: the type of types is now called ty, not t

parent 081bcb5c
...@@ -13,7 +13,7 @@ transformation "simplify_recursive_definition" ...@@ -13,7 +13,7 @@ transformation "simplify_recursive_definition"
transformation "inline_trivial" transformation "inline_trivial"
transformation "eliminate_builtin" transformation "eliminate_builtin"
transformation "eliminate_definition"(*_func"*) transformation "eliminate_definition" (*_func*)
transformation "eliminate_inductive" transformation "eliminate_inductive"
transformation "eliminate_algebraic" transformation "eliminate_algebraic"
transformation "eliminate_if" transformation "eliminate_if"
......
...@@ -66,7 +66,7 @@ module Utils = struct ...@@ -66,7 +66,7 @@ module Utils = struct
(** type representing types *) (** type representing types *)
let t = Ty.create_tysymbol (id_fresh "t") [] None let t = Ty.create_tysymbol (id_fresh "ty") [] None
let my_t = ty_app t [] let my_t = ty_app t []
let t_decl = Decl.create_ty_decl [(t, Tabstract)] let t_decl = Decl.create_ty_decl [(t, Tabstract)]
......
...@@ -14,6 +14,7 @@ theory Test_ind ...@@ -14,6 +14,7 @@ theory Test_ind
goal G : true goal G : true
end end
(*
theory Test_encoding theory Test_encoding
use import int.Int use import int.Int
logic id(x: int) : int = x logic id(x: int) : int = x
...@@ -28,6 +29,7 @@ theory Test_encoding ...@@ -28,6 +29,7 @@ theory Test_encoding
(forall x:int. x=x+1) (forall x:int. x=x+1)
goal G2 : forall x:int. let x = 0 + 1 in x = let y = 0 + 1 + 0 in y goal G2 : forall x:int. let x = 0 + 1 in x = let y = 0 + 1 + 0 in y
end end
*)
theory Test_simplify_array theory Test_simplify_array
use import array.Array use import array.Array
......
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