Handle morphisms

Following the method described in the paper Kazuhiko Sakaguchi Reflexive tactics for algebra, revisited
math-comp · May 9, 2022 · e3c7a67 · e3c7a67
1 parent 35338c4
commit e3c7a67
Show file tree

Hide file tree

Showing 3 changed files with 395 additions and 213 deletions.
diff --git a/examples/lra_examples.v b/examples/lra_examples.v
@@ -258,8 +258,8 @@ Qed.
 
 Goal ratr (1 / 2%:R) = 1 / 2%:R :> F.
 Proof.
-Fail lra.  (* TODO should work *)
-Abort.
+lra.
+Qed.
 
 Goal 1 ^+ (2 + 2) = 1 :> F.
 Proof.