hacspec_translation_modificatons.txt

`:>` becomes `::` (version based syntax)

Order in type class of generated elements from trait
- f_Z_t_Field moved up, and t_PartialEq got an extra f_Z added

Import names changed:
```
Require Import Crate_Ovn_traits.
Export Crate_Ovn_traits.
```
becomes
```
From OVN Require Import Hacspec_ovn_Ovn_traits.
Export Hacspec_ovn_Ovn_traits.
```

Put type class instances into section context, that is move function arguments of the form
```
 {v_Z : _} `{ t_Sized v_Z} `{ t_Field v_Z}
```
to the top of the section. Helps Coq resolve call dependencies. This also requires fixing one some type annotations, by removing the extra arguments.


Add:
```coq
  Solve All Obligations with now intros ; destruct from_uint_size.
```
to help resolve obligations, for memory loctions.

Comment away `t_ParseError` from `letm[ _ ]` (incorrect infered type)

Comment away `t_ControlFlow` (does not exists)

Comment away `ParseError` does not exists and incorrect type.

Replace not with negb, incorrect name!

Add Result_Ok to accumulator for foldi_both_list, incorrect type?

List of replacements or removed objects.
  (* {v_Z : _} `{ t_Sized v_Z} `{ t_Field v_Z} *)
  (* {v_G : _} `{ t_Sized v_G} `{ t_Group v_G} *)
  (* t_SchnorrZKPCommit v_G *)
  (* t_OrZKPCommit v_G *)
  (* {v_G : _} {n : both uint_size} `{ t_Sized v_G} `{ t_Group v_G} *)
  (* t_OvnContractState v_G (both uint_size) *)
  (*  {v_G : _} {n : both uint_size} {v_A : _} {impl_574521470_ : _} `{ t_Sized v_G} `{ t_Sized v_A} `{ t_Sized impl_574521470_} `{ t_Group v_G} `{ t_HasActions v_A} `{ t_HasReceiveContext impl_574521470_ 'unit} *)
  (* impl_574521470_ -> t_CastVoteParam or t_RegisterParam or t_TallyParameter *)

Need to add instantionations.
```
Context {v_G : choice_type}.

(* TODO: Cannot find instance in hacspec lib? *)
Instance v_G_t_copy : t_Copy v_G := _.
Instance v_G_t_partial_eq : t_PartialEq v_G v_G := _.
Instance v_G_t_eq : t_Eq v_G := _.
Instance v_G_t_clone : t_Clone v_G := _.
Instance v_G_t_serialize : t_Serialize v_G := _.

Context {v_G_t_Group : t_Group v_G}.
Instance v_G_t_Group_temp : t_Group v_G := v_G_t_Group.

Context {v_A : choice_type}.
Context {v_A_t_Sized : t_Sized v_A}.
Instance v_A_t_Sized_temp : t_Sized v_A := v_A_t_Sized.

Context {v_A_t_HasActions : t_HasActions v_A}.
Instance v_A_t_HasActions_temp : t_HasActions v_A := v_A_t_HasActions.

Context {n : both uint_size}.

(* Extra from code *)
Context {v_G_t_Sized : t_Sized v_G}.
Instance v_G_t_Sized_temp : t_Sized v_G := v_G_t_Sized.

Notation v_Z := f_Z.
```