From 661940fd55a925a6f17f6025f5d15fc9f5647cf9 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 10 Oct 2016 10:59:22 +0200
Subject: Put all plugins behind an "API".

---
 API/API.ml | 215 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 215 insertions(+)
 create mode 100644 API/API.ml

(limited to 'API/API.ml')

diff --git a/API/API.ml b/API/API.ml
new file mode 100644
index 0000000000..2b7bbd561b
--- /dev/null
+++ b/API/API.ml
@@ -0,0 +1,215 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module Ppvernac = Ppvernac
+module Command = Command
+module States = States
+module Kindops = Kindops
+module Coq_config = Coq_config
+module Esubst = Esubst
+module Evar = Evar
+module Constrexpr = Constrexpr
+module Libobject = Libobject
+module Evd = Evd
+module Libnames = Libnames
+module Nameops = Nameops
+module Topfmt = Topfmt
+module Locus = Locus
+module Locusops = Locusops
+module Lemmas = Lemmas
+module Clenv = Clenv
+module Elimschemes = Elimschemes
+module Classes = Classes
+module Class_tactics = Class_tactics
+module Eauto = Eauto
+module Keys = Keys
+module Vernac_classifier = Vernac_classifier
+module Autorewrite = Autorewrite
+module Redops = Redops
+module Elim = Elim
+module Geninterp = Geninterp
+module Obligations = Obligations
+module Retroknowledge = Retroknowledge
+module Evar_refiner = Evar_refiner
+module Hipattern = Hipattern
+module Auto = Auto
+module Hints = Hints
+module Contradiction = Contradiction
+module Tacticals = Tacticals
+module Tactics = Tactics
+module Inv = Inv
+module Leminv = Leminv
+module Equality = Equality
+module Redexpr = Redexpr
+module Pfedit = Pfedit
+module Stm = Stm
+module Stateid = Stateid
+module Declaremods = Declaremods
+module Miscops = Miscops
+module Miscprint = Miscprint
+module Genprint = Genprint
+module Ppconstr = Ppconstr
+module Pputils = Pputils
+module Extend = Extend
+module Logic = Logic
+module Himsg = Himsg
+module Tacred = Tacred
+module Names = Names
+module Indrec = Indrec
+module Glob_ops = Glob_ops
+module Constrexpr_ops = Constrexpr_ops
+module Eqdecide = Eqdecide
+module Genredexpr = Genredexpr
+module Detyping = Detyping
+module Tactypes = Tactypes
+module ExplainErr = ExplainErr
+module Printer = Printer
+module Constrextern = Constrextern
+module Locality = Locality
+module Impargs = Impargs
+module Termops = Termops
+module Refiner = Refiner
+module Ppextend = Ppextend
+module Nametab = Nametab
+module Vernacentries = Vernacentries
+module Mltop = Mltop
+module Goal = Goal
+module Proof_global = Proof_global
+module Proof = Proof
+module Smartlocate = Smartlocate
+module Dumpglob = Dumpglob
+module Constrintern = Constrintern
+module Topconstr = Topconstr
+module Notation_ops = Notation_ops
+module Patternops = Patternops
+module Mod_typing = Mod_typing
+module Modops = Modops
+module Opaqueproof = Opaqueproof
+module Ind_tables = Ind_tables
+module Typeops = Typeops
+module Inductive = Inductive
+module Vars = Vars
+module Reduction = Reduction
+module Mod_subst = Mod_subst
+module Sorts = Sorts
+module Univ = Univ
+module Constr = Constr
+module CClosure = CClosure
+module Type_errors = Type_errors
+module Safe_typing = Safe_typing
+module UGraph = UGraph
+module Namegen = Namegen
+module Ftactic = Ftactic
+module UState = UState
+module Proofview_monad = Proofview_monad
+module Classops = Classops
+module Global = Global
+module Goptions = Goptions
+module Lib = Lib
+module Library = Library
+module Summary = Summary
+module Universes = Universes
+module Declare = Declare
+module Refine = Refine
+module Find_subterm = Find_subterm
+module Evar_kinds = Evar_kinds
+module Decl_kinds = Decl_kinds
+module Misctypes = Misctypes
+module Pattern = Pattern
+module Vernacexpr = Vernacexpr
+module Search = Search
+module Notation_term = Notation_term
+module Reductionops = Reductionops
+module Inductiveops = Inductiveops
+module Recordops = Recordops
+module Retyping = Retyping
+module Typing = Typing
+module Evarsolve = Evarsolve
+module Constr_matching = Constr_matching
+module Pretyping = Pretyping
+module Evarconv = Evarconv
+module Unification = Unification
+module Typeclasses = Typeclasses
+module Pretype_errors = Pretype_errors
+module Notation = Notation
+module Declarations = Declarations
+module Declareops = Declareops
+module Globnames = Globnames
+module Environ = Environ
+module Term = Term
+module Coqlib = Coqlib
+module Glob_term = Glob_term
+module Context = Context
+module Stdarg = Stdarg
+module Tacmach = Tacmach
+module Proofview = Proofview
+module Evarutil = Evarutil
+module EConstr = EConstr
+
+module Prelude =
+  struct
+    type global_reference = Globnames.global_reference
+    type metavariable = int
+    type meta_value_map = (metavariable * Constr.constr) list
+    type named_context_val = Environ.named_context_val
+    type conv_pb = Reduction.conv_pb =
+      | CONV
+      | CUMUL
+    type constr = Constr.constr
+    type types = Constr.types
+    type evar = Constr.existential_key
+    type 'constr pexistential = 'constr Constr.pexistential
+    type env = Environ.env
+    type evar_map = Evd.evar_map
+    type rigid = Evd.rigid =
+               | UnivRigid
+               | UnivFlexible of bool
+    type reference = Libnames.reference =
+      | Qualid of Libnames.qualid Loc.located
+      | Ident of Names.Id.t Loc.located
+  end
+
+(* NOTE: It does not make sense to replace the following "module expression"
+   simply with "module Proof_type = Proof_type" because
+   there is only "kernel/entries.mli";
+   there is no "kernel/entries.ml" file *)
+module Entries =
+  struct
+    type mutual_inductive_entry = Entries.mutual_inductive_entry
+    type inline = int option
+    type 'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
+    type 'a const_entry_body = 'a proof_output Future.computation
+    type 'a definition_entry = 'a Entries.definition_entry =
+                                 { const_entry_body   : 'a const_entry_body;
+                                   const_entry_secctx : Context.Named.t option;
+                                   const_entry_feedback : Stateid.t option;
+                                   const_entry_type        : Term.types option;
+                                   const_entry_polymorphic : bool;
+                                   const_entry_universes   : Univ.universe_context;
+                                   const_entry_opaque      : bool;
+                                   const_entry_inline_code : bool }
+    type parameter_entry = Entries.parameter_entry
+    type projection_entry = Entries.projection_entry
+    type 'a constant_entry = 'a Entries.constant_entry =
+                           | DefinitionEntry of 'a definition_entry
+                           | ParameterEntry of parameter_entry
+                           | ProjectionEntry of projection_entry
+  end
+
+(* NOTE: It does not make sense to replace the following "module expression"
+   simply with "module Proof_type = Proof_type" because
+   there is only "proofs/proof_type.mli";
+   there is no "proofs/proof_type.ml" file *)
+module Proof_type =
+  struct
+    type goal = Goal.goal
+    type tactic = goal Evd.sigma -> goal list Evd.sigma
+    type rule = Proof_type.prim_rule =
+      | Cut of bool * bool * Names.Id.t * Term.types
+      | Refine of Term.constr
+  end
-- 
cgit v1.2.3