Ncring_tac: don't use pairs to handle extensibility

doc/changelog/04-tactics/19501-ncring-tac-speed.rst

@@ -0,0 +1,7 @@
+- **Changed:**
+  `Ncring_tac.extra_reify` is expected to return `tt` on failure and
+  the reification result on success, instead of `(false, anything)` on failure
+  and `(true, result)` on success
+  (this only matters to users overriding it to extend the Ncring reification)
+  (`#19501 <https://github.com/coq/coq/pull/19501>`_,
+  by Gaëtan Gilbert).

theories/nsatz/Nsatz.v

@@ -68,13 +68,13 @@ try (try apply Rsth;
 Defined.
 
 Ltac extra_reify term ::=
-  match term with
+  lazymatch term with
   | IZR ?z =>
-      match isZcst z with
-      | true => open_constr:((true, PEc z))
-      | false => open_constr:((false,tt))
+      lazymatch isZcst z with
+      | true => open_constr:(PEc z)
+      | false => open_constr:(tt)
       end
-  | _ => open_constr:((false,tt))
+  | _ => open_constr:(tt)
   end.
 
 Lemma R_one_zero: 1%R <> 0%R.

theories/setoid_ring/Ncring_tac.v

@@ -50,7 +50,9 @@ Ltac close_varlist lvar :=
   | _ => let _ := constr:(eq_refl : lvar = @nil _) in idtac
   end.
 
-Ltac extra_reify term := open_constr:((false,tt)).
+(* extensibility: override to add ways to reify a term.
+   Return [tt] for terms which aren't handled (tt doesn't have type PExpr so is unambiguous) *)
+Ltac extra_reify term := open_constr:(tt).
 
 Ltac reify_term Tring lvar term :=
   match open_constr:((Tring, term)) with
@@ -112,10 +114,10 @@ Ltac reify_term Tring lvar term :=
   | _ =>
       let extra := extra_reify term in
       lazymatch extra with
-      | (false,_) =>
+      | tt =>
         let n := reify_as_var lvar term in
         open_constr:(PEX Z (Pos.of_succ_nat n))
-      | (true,?v) => v
+      | ?v => v
       end
   end.