# Faq

Here we answer to some questions you may have when using `coq-of-ocaml`

.

## Why is there an `-impredicative-set`

option to Coq?

To compile the files generated by `coq-of-ocaml`

, we need to use the `-impredicative-set`

option with Coq. The Impredicative Set page of the Coq wiki gives some details about this option. The reason for that is to avoid getting into universe inconsistency errors. If we take the following example:

`type t =`

| Empty

| Node : 'a -> t

(* This function could be a deserializing function from [string] to [t]. We

use lists for the sake of simplicity. *)

let rec t_of_list (l : 'a list) : t =

match l with

| [] -> Empty

| _ :: l -> Node (t_of_list l)

we generate the Coq translation:

`Require Import CoqOfOCaml.CoqOfOCaml.`

Require Import CoqOfOCaml.Settings.

Inductive t : Set :=

| Empty : t

| Node : forall {a : Set}, a -> t.

Fixpoint t_of_list {a : Set} (l : list a) : t :=

match l with

| [] => Empty

| cons _ l => Node (t_of_list l)

end.

The type `t`

has a constructor `Node`

with an existential type `a`

. With the function `t_of_list`

we generate a value with a number of nested existential types equals to the length of the list `l`

. This generated Coq code is valid.

In contrast, if we were using `Type`

instead of `Set`

this would not work. Indeed, an existential type increases the universe level by one in `Type`

. So this function would have a universe level for its result equals to the length on the list. This does not seem easy to express, even with polymorphic universes.