Handle morphisms

Following the method described in the paper Kazuhiko Sakaguchi Reflexive tactics for algebra, revisited
math-comp · May 11, 2022 · ec8e304 · ec8e304
1 parent 5381470
commit ec8e304
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.
-Original file line number
+Diff line change
@@ Expand Up / @@ -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.
@@ Expand Down @@