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.

2 files changed, 10 insertions, 4 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
diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v
index 46ffa083f..d95f35bf4 100644
--- a/src/PushButtonSynthesis/WordByWordMontgomery.v
+++ b/src/PushButtonSynthesis/WordByWordMontgomery.v
@@ -235,10 +235,11 @@ Section __.
           (CorrectnessStringification.dyn_context.cons
              r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)")%string
              (CorrectnessStringification.dyn_context.cons
-                from_montgomery_res (prefix ++ "from_montgomery")%string
+                from_montgomery_res "from_montgomery"%string
                 (CorrectnessStringification.dyn_context.cons
                    (@eval 8 n_bytes) "bytes_eval"%string
-                   CorrectnessStringification.dyn_context.nil)))).
+                   CorrectnessStringification.dyn_context.nil))))
+         (only parsing).
   Local Notation stringify_correctness prefix pre_extra correctness
     := (stringify_correctness_with_ctx
           (initial_ctx prefix)