Commit f9d6ff78 authored by MARCHE Claude's avatar MARCHE Claude

investigate bts 20881

parent 854c219b
theory OK
type t 'a = A | B (t 'a)
goal g : forall x: t 'a. A <> B x
end
theory Bug1
type t 'a = A int
function f (t 'a) : 'a
goal g : let p = (A 0: t int) in
let q = (A 1: t int) in
f p = f q
end
theory Bug
use import map.Map
......
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