Intended for reviewing the changes wrt. the hide trick

[DmxLarchey]

This PR draft is intended for reviewing the changes required to implement the hide trick that erases tricky __ : Obj.t arguments (which implement a loop) in the Ocaml extracted code.

This gives the following extracted code:

type nat =
| O
| S of nat

type 'a sig0 = 'a
  (* singleton inductive, whose constructor was exist *)

(** val vec_prj : 'a1 list -> nat -> 'a1 **)

let rec vec_prj u i =
  match u with
  | [] -> assert false (* absurd case *)
  | x::v -> (match i with
             | O -> x
             | S j -> vec_prj v j)

type recalg =
| Ra_zero
| Ra_succ
| Ra_proj of nat
| Ra_comp of recalg * recalg list
| Ra_prec of recalg * recalg
| Ra_umin of recalg

(** val vec_map_compute : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec vec_map_compute fcomp = function
| [] -> []
| x::xa -> (fcomp x)::(vec_map_compute fcomp xa)

(** val prim_rec_compute :
    ('a1 -> 'a2) -> ('a1 -> nat -> 'a2 -> 'a2) -> 'a1 -> nat -> 'a2 **)

let rec prim_rec_compute fcomp gcomp x = function
| O -> fcomp x
| S n -> gcomp x n (prim_rec_compute fcomp gcomp x n)

(** val umin_compute : (nat -> nat) -> nat -> nat **)

let rec umin_compute f s =
  match f s with
  | O -> s
  | S _ -> umin_compute f (S s)

(** val ra_compute : recalg -> nat list -> nat **)

let rec ra_compute sk vk =
  match sk with
  | Ra_zero -> O
  | Ra_succ ->
    (match vk with
     | [] -> assert false (* absurd case *)
     | y::_ -> S y)
  | Ra_proj i -> vec_prj vk i
  | Ra_comp (sb, skb) ->
    ra_compute sb (vec_map_compute (fun p -> ra_compute p vk) skb)
  | Ra_prec (sb, sb'') ->
    (match vk with
     | [] -> assert false (* absurd case *)
     | y::u ->
       prim_rec_compute (fun p -> ra_compute sb p) (fun v n x ->
         ra_compute sb'' (n::(x::v))) u y)
  | Ra_umin sb' -> umin_compute (fun p -> ra_compute sb' (p::vk)) O