Commit ac976a84 authored by Andrei Paskevich's avatar Andrei Paskevich

fix the discriminator function

parent dc84e0b3
......@@ -251,8 +251,8 @@ let add_discriminator (state,task) ts ty csl =
let ax = t_forall_close (List.rev ul) [[t1]] ax in
add_prop_decl task Paxiom pr ax
in
let dl_add task = function
| c :: cl -> List.fold_left (d_add c) task cl
let rec dl_add task = function
| c :: cl -> dl_add (List.fold_left (d_add c) task cl) cl
| _ -> task
in
state, dl_add task csl
......
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