Drop `map λ` bits in docstrings

They are redundant with the bounds pre- and post-conditions in WBW
montgomery.

Also drop the fiat_p... prefix from the `from_montgomery` bits in most
of the docstrings, under the assumption that shorter strings with less
repetition are more readable.

1 files changed, 7 insertions, 2 deletions

diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v
index ee2793c40..4d3e9c047 100644
--- a/src/PushButtonSynthesis/Primitives.v
+++ b/src/PushButtonSynthesis/Primitives.v
@@ -183,6 +183,9 @@ Module CorrectnessStringification.
       => strip_bounds_info T
     | list_Z_bounded_by _ _ -> ?T
       => strip_bounds_info T
+    | (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c) -> ?T
+      => let T := strip_bounds_info T in
+         constr:(a <= b < c -> T)
     | ?T /\ list_Z_bounded_by _ _
       => T
     | ?T /\ (match _ with pair _ _ => _ end = true)
@@ -191,8 +194,10 @@ Module CorrectnessStringification.
       => T
     | iff _ _
       => correctness
-    | _ = _ /\ (_ = _ /\ (_ <= _ < _))
-      => correctness
+    | ?x = ?y /\ (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c)
+      => constr:(x = y /\ a <= b < c)
+    | (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c)
+      => constr:(a <= b < c)
     | _ = _ :> list Z
       => correctness
     | forall x : ?T, ?f