Library MetaCoq.Template.Extraction
Extraction setup for template-coq.
From Coq Require Ascii Extraction ZArith NArith.
From MetaCoq.Template Require Import utils Ast Reflect Induction.
From Coq Require Import FSets ExtrOcamlBasic ExtrOCamlFloats
ExtrOCamlInt63.
From MetaCoq.Template Require Import MC_ExtrOCamlZPosInt.
Extract Inductive Decimal.int ⇒ unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
Extract Inductive Hexadecimal.int ⇒ unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
Extract Inductive Number.int ⇒ unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
Extract Inductive Equations.Init.sigma ⇒ "( * )" ["(,)"].
Extract Constant Equations.Init.pr1 ⇒ "fst".
Extract Constant Equations.Init.pr2 ⇒ "snd".
Extraction Inline Equations.Init.pr1 Equations.Init.pr2.
Extraction Blacklist Classes config uGraph Universes Ast String List Nat Int
UnivSubst Typing Checker Retyping OrderedType Logic Common Equality UnivSubst Numeral
Uint63.
Set Warnings "-extraction-opaque-accessed".
Set Warnings "-extraction-reserved-identifier".
From MetaCoq.Template Require Import TemplateMonad.Extractable config Induction
LiftSubst UnivSubst Pretty TemplateProgram.
Import Init.Nat.
Extract Constant Typing.guard_checking ⇒ "{ fix_guard = (fun _ _ _ -> true); cofix_guard = (fun _ _ _ -> true) }".
Cd "gen-src".
Set Warnings "-extraction-logical-axiom".
Separate Extraction FloatOps.Prim2SF.
Recursive Extraction Library Extractable.
Extraction Library MCPrelude.
Extraction Library MCOption.
Extraction Library MCUtils.
Extraction Library MCList.
Extraction Library EqDecInstances.
Extraction Library Induction.
Extraction Library LiftSubst.
Extraction Library UnivSubst.
Extraction Library BasicAst.
Extraction Library Reflect.
Extraction Library Pretty.
Extraction Library config.
Recursive Extraction Library TemplateProgram.
Cd "..".