eunify.ref

"eunify_test"
     : string
The command has indeed failed with message:
No matching clauses for match.
((fix add (n m : nat) {struct n} : nat :=
    match n with
    | 0 => m
    | S p => S (add p m)
    end) x y)
"eunify_test_evars"
     : string
The command has indeed failed with message:
No matching clauses for match.