Commit 80cd98c6 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[qed] merge terms with type Bool and Prop

parent 195c9f9e
...@@ -235,6 +235,7 @@ struct ...@@ -235,6 +235,7 @@ struct
match t1, t2 with match t1, t2 with
| None, None -> true | None, None -> true
| None, Some _ | Some _ , None -> false | None, Some _ | Some _ , None -> false
| Some (Bool|Prop) , Some(Bool|Prop) -> true
| Some t1, Some t2 -> Tau.equal t1 t2 | Some t1, Some t2 -> Tau.equal t1 t2
let sort x = x.sort let sort x = x.sort
......
Supports Markdown
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