Commit 048ada9b authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

corrected a bug in term.ml

parent 5e23731c
Pipeline #1640 failed with stage
in 12 seconds
......@@ -1135,7 +1135,7 @@ let simple_normalize : type a. environement -> a term -> a term = fun env t ->
begin
match eiv env n_u with
| Fun ("pair",x :: [y]) -> y
| _ -> Fun ("pi1", [n_u])
| _ -> Fun ("pi2", [n_u])
end
| Fun ("dec", u :: [sk]) ->
......
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