(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** Extraction to Ocaml : use of basic Ocaml types *)

Extract Inductive bool => bool [ true false ].
Extract Inductive option => option [ Some None ].
Extract Inductive prod => "( * )" [ "" ].
 (* The "" above is a hack, but produce nicer code than with "(,)" *)
Extract Inductive unit => unit [ "()" ].
Extract Inductive list => list [ "[]" "( :: )" ].

(** We could also map sumbool to bool, sumor to option, but
    this isn't always a gain in clarity. We leave it to the user...

Extract Inductive sumbool => bool [ true false ].
Extract Inductive sumor => option [ Some None ].
*)

(** Restore lazyness of andb, orb.
    NB: without these Extract Constant, andb/orb would be inlined
    by extraction in order to have lazyness, producing inelegant
    (if ... then ... else false) and (if ... then true else ...).
*)

Extract Inlined Constant andb => "(&&)".
Extract Inlined Constant orb => "(||)".