diff options
| author |  jadep <jade.philipoom@gmail.com> | 2019-04-03 14:45:32 -0400 |
|---|---|---|
| committer | jadephilipoom <jade.philipoom@gmail.com> | 2019-04-03 23:34:53 +0100 |
| commit | bd34d676010ebf6dd4aa5076537f89572803dd3d (patch) | |
| tree | bbc634fa51d071a4bd1e55019dc6853ecd936622 /src/PushButtonSynthesis/Primitives.v | |
| parent | ee30e8faf778ac9fd43f1d8d9d6d61cd4e9d8b3f (diff) | |
partition -> Partition.partition to prevent confusion with List.partition
Diffstat (limited to 'src/PushButtonSynthesis/Primitives.v')
| -rw-r--r-- | src/PushButtonSynthesis/Primitives.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 93c2e4c69..a3df39c25 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -574,7 +574,7 @@ Module CorrectnessStringification. Ltac stringify ctx correctness fname arg_var_data out_var_data := let G := match goal with |- ?G => G end in let correctness := (eval hnf in correctness) in - let correctness := (eval cbv [partition WordByWordMontgomery.valid WordByWordMontgomery.small] in correctness) in + let correctness := (eval cbv [Partition.partition WordByWordMontgomery.valid WordByWordMontgomery.small] in correctness) in let correctness := strip_bounds_info correctness in let arg_var_names := constr:(type.map_for_each_lhs_of_arrow (@ToString.C.OfPHOAS.names_of_var_data) arg_var_data) in let out_var_names := constr:(ToString.C.OfPHOAS.names_of_base_var_data out_var_data) in |