refactor(coq): reintroduce Value type for coq_config

As was pointed out in my silly PR getting rid of it, it introduces an
extra boxing that is unneeded.

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: 2f6b0e94-1350-446a-810d-bfc6c34ae46e -->

Author: Alizter

src/dune_rules/coq/coq_config.ml

@@ -44,6 +44,13 @@ end = struct
   let get_path t var = get t var |> Path.of_string
 end
 
+module Value = struct
+  type t =
+    | Int of int
+    | Path of Path.t
+    | String of string
+end
+
 module Version = struct
   module Num = struct
     type t =
@@ -83,9 +90,9 @@ module Version = struct
 
     let by_name { major; minor; suffix } name =
       match name with
-      | "major" -> Some (`Int major)
-      | "minor" -> Some (`Int minor)
-      | "suffix" -> Some (`String suffix)
+      | "major" -> Some (Value.Int major)
+      | "minor" -> Some (Value.Int minor)
+      | "suffix" -> Some (Value.String suffix)
       | _ -> None
   end
 
@@ -132,8 +139,8 @@ module Version = struct
       | "version.minor" -> Num.by_name version_num "minor"
       | "version.revision" -> Num.by_name version_num "revision"
       | "version.suffix" -> Num.by_name version_num "suffix"
-      | "version" -> Some (`String version_string)
-      | "ocaml-version" -> Some (`String ocaml_version_string)
+      | "version" -> Some (Value.String version_string)
+      | "ocaml-version" -> Some (Value.String ocaml_version_string)
       | _ -> None)
 end
 
@@ -205,6 +212,7 @@ let by_name { version_info; coqlib; coq_native_compiler_default } name =
   | "version.suffix"
   | "version"
   | "ocaml-version" -> Version.by_name version_info name
-  | "coqlib" -> Some (`Path coqlib)
-  | "coq_native_compiler_default" -> Some (`String coq_native_compiler_default)
+  | "coqlib" -> Some (Value.Path coqlib)
+  | "coq_native_compiler_default" ->
+    Some (Value.String coq_native_compiler_default)
   | _ -> None

src/dune_rules/coq/coq_config.mli

@@ -9,5 +9,20 @@ val make : coqc:Action.Prog.t -> t Memo.t
 
 val make_opt : coqc:Action.Prog.t -> t Option.t Memo.t
 
-val by_name :
-  t -> string -> [> `Int of int | `Path of Path.t | `String of string ] Option.t
+module Value : sig
+  type t =
+    | Int of int
+    | Path of Path.t
+    | String of string
+end
+
+(** [by_name t name] returns the value of the option [name] in the Coq
+    configuration [t]. Currently supported names are:
+
+    - version.major
+    - version.minor
+    - version.revision
+    - version.suffix
+    - version
+    - ocaml-version *)
+val by_name : t -> string -> Value.t Option.t

src/dune_rules/coq/coq_rules.ml

@@ -29,7 +29,7 @@ let select_native_mode ~sctx ~dir (buildable : Coq_stanza.Buildable.t) =
       | None -> Coq_mode.VoOnly
       | Some config -> (
         match Coq_config.by_name config "coq_native_compiler_default" with
-        | Some (`String "yes") | Some (`String "ondemand") -> Coq_mode.Native
+        | Some (String "yes") | Some (String "ondemand") -> Coq_mode.Native
         | _ -> Coq_mode.VoOnly))
 
 (* CR alizter: move this to Lib.DB *)

src/dune_rules/expander.ml

@@ -627,9 +627,9 @@ let expand_pform_gen ~(context : Context.t) ~bindings ~dir ~source
                   [ Pp.textf "Unknown Coq configuration variable %S" s ]
               | Some v -> (
                 match v with
-                | `Int x -> string (string_of_int x)
-                | `String x -> string x
-                | `Path x -> Value.L.paths [ x ])))))
+                | Int x -> string (string_of_int x)
+                | String x -> string x
+                | Path x -> Value.L.paths [ x ])))))
 
 (* Make sure to delay exceptions *)
 let expand_pform_gen ~context ~bindings ~dir ~source pform =