Skip to content
Snippets Groups Projects
Verified Commit 1d434b81 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

fix trait inclusion

parent 06e7a80b
No related branches found
No related tags found
No related merge requests found
Pipeline #117247 passed
......@@ -3455,11 +3455,11 @@ Ltac find_trait_term cont :=
strip_applied_params a (hnil id) ltac:(fun a acc =>
is_projection a;
match a with
| (?c1 ?c2) ?d =>
| ?c1 ?d =>
(* d should be the spec parameter *)
is_var d;
(* c2 is the implicit params parameter *)
is_var c2;
(*is_var c2;*)
cont c1 d acc
end)
end
......@@ -3470,9 +3470,9 @@ Ltac prove_trait_incl_for trait_spec trait_proj appspec cont :=
lazymatch goal with
| H : trait_incl_marker (?incl trait_spec ?spec2) |- _ =>
let H2 := fresh in
let t1 := constr:(trait_proj _ trait_spec) in
let t1 := constr:(trait_proj trait_spec) in
let t1 := apply_term_het constr:(t1) constr:(appspec) in
let t2 := constr:(trait_proj _ spec2) in
let t2 := constr:(trait_proj spec2) in
let t2 := apply_term_het constr:(t2) constr:(appspec) in
assert (function_subtype t1 t2) as H2;
[ rewrite trait_incl_marker_unfold in H; apply H | cont H2]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment