Commit d13a76d0 authored by Andrei Paskevich's avatar Andrei Paskevich

rename Explicit_polymorphism to Encoding_explicit

parent 56c75ea6
......@@ -107,14 +107,14 @@ LIB_PARSER = ptree parser lexer denv typing
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf
LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
split_conjunction \
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
inlining split_conjunction split_goal \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
encoding_enumeration encoding encoding_decorate_mono \
libencoding encoding_decorate encoding_bridge \
explicit_polymorphism encoding_simple encoding_simple2 encoding_instantiate \
simplify_array filter_trigger split_goal
encoding_explicit encoding_simple encoding_simple2 \
encoding_instantiate simplify_array filter_trigger
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa
......
......@@ -75,8 +75,8 @@ let ls_of_const =
let ls_of_t t = match t.t_node with
| Tconst _ ->
begin try Hterm.find ht t with Not_found ->
let s = Pp.string_of Pretty.print_term t in
let ls = create_fsymbol (id_fresh ("const_" ^ s)) [] ty_base in
let s = "const_" ^ Pp.string_of Pretty.print_term t in
let ls = create_fsymbol (id_fresh s) [] ty_base in
Hterm.add ht t ls;
ls
end
......
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