Commit 6be4bcf6 authored by MARCHE Claude's avatar MARCHE Claude

test poly with defined projections

parent 27d0254c
......@@ -804,4 +804,3 @@ let make_record_pattern kn fll ty =
| None -> pat_wild (ty_inst s (Opt.get pj.ls_value))
in
pat_app cs (List.map get_arg pjl) ty
......@@ -28,6 +28,14 @@ with b = G | H a
goal g3 : forall x. x <> F (H x)
type v = I (p:t) | J (p:t) u
constant x : v
goal g4 : match x with I y -> y=A | J y (D z) -> z=A | J B z -> z=C | J A C -> true end
goal g5 : match x with I y -> y | J y _ -> y end = A
end
......
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