[skip ci] Z3encoding: documenting the function style for the context

compiler/verification/z3encoding.ml

@@ -35,6 +35,12 @@ type context = {
       (* A map from strings, corresponding to Z3 symbol names, to the Catala variable they
          represent. Used when to pretty-print Z3 models when a counterexample is generated *)
 }
+(** The context contains all the required information to encode a VC represented as a Catala term to
+    Z3. The fields [ctx_decl] and [ctx_var] are computed before starting the translation to Z3, and
+    are thus unmodified throughout the translation. The [ctx_z3] context is an OCaml abstraction on
+    top of an underlying C++ imperative implementation, it is therefore only created once.
+    Unfortunately, the maps [ctx_funcdecl] and [ctx_z3vars] are computed dynamically during the
+    translation requiring us to pass the context around in a functional way **)
 
 (** [add_funcdecl] adds the mapping between the Catala variable [v] and the Z3 function declaration
     [fd] to the context **)