Commit fb1712dd authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Make f_contractive more robust.

parent d237e729
Pipeline #3517 passed with stage
in 10 minutes and 42 seconds
......@@ -179,7 +179,8 @@ Ltac f_contractive :=
| |- ?f _ _ {_} ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f)
end;
try match goal with
| |- dist_later ?n ?x ?y => destruct n as [|n]; [done|change (x {n} y)]
| |- @dist_later ?A ?n ?x ?y =>
destruct n as [|n]; [done|change (@dist A _ n x y)]
end;
try reflexivity.
......
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