aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.gitignore2
-rw-r--r--API/API.ml286
-rw-r--r--API/API.mli6247
-rw-r--r--API/API.mllib1
-rw-r--r--API/PROPERTIES8
-rw-r--r--META.coq15
-rw-r--r--Makefile.build8
-rw-r--r--Makefile.common4
-rw-r--r--Makefile.dev2
-rw-r--r--Makefile.doc2
-rw-r--r--config/coq_config.mli1
-rw-r--r--configure.ml5
-rw-r--r--dev/base_include4
-rw-r--r--dev/ci/user-overlays/06493-gares-API-remove-big-file.sh8
-rw-r--r--dev/core.dbg1
-rw-r--r--dev/doc/changes.md10
-rw-r--r--dev/ocamldebug-coq.run1
-rw-r--r--dev/top_printers.ml2
-rw-r--r--lib/coqProject_file.ml410
-rw-r--r--lib/coqProject_file.mli1
-rw-r--r--plugins/.merlin1
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--tactics/tacticals.mli2
-rwxr-xr-xtest-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh36
-rwxr-xr-xtest-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh31
-rw-r--r--test-suite/coq-makefile/template/src/test.ml41
-rw-r--r--test-suite/coq-makefile/template/src/test_aux.ml2
-rw-r--r--test-suite/coq-makefile/template/src/test_aux.mli2
-rw-r--r--tools/CoqMakefile.in2
-rw-r--r--tools/coq_makefile.ml13
30 files changed, 29 insertions, 6681 deletions
diff --git a/.gitignore b/.gitignore
index cec51986d..27ac0631a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -82,8 +82,6 @@ test-suite/coq-makefile/*/html
test-suite/coq-makefile/*/mlihtml
test-suite/coq-makefile/*/subdir/done
test-suite/coq-makefile/merlin1/.merlin
-test-suite/coq-makefile/plugin-reach-outside-API-and-fail/_CoqProject
-test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/_CoqProject
test-suite/coqdoc/Coqdoc.*
test-suite/coqdoc/index.html
test-suite/coqdoc/coqdoc.css
diff --git a/API/API.ml b/API/API.ml
deleted file mode 100644
index 081ac2bb2..000000000
--- a/API/API.ml
+++ /dev/null
@@ -1,286 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* Warning, this file respects the dependency order established in Coq.
-
- To see such order issue the comand:
-
- ```
- bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done > API/link
- ```
- *)
-
-(******************************************************************************)
-(* config *)
-(******************************************************************************)
-module Coq_config = Coq_config
-
-(******************************************************************************)
-(* Kernel *)
-(******************************************************************************)
-(* "mli" files *)
-module Declarations = Declarations
-module Entries = Entries
-
-module Names = Names
-(* module Uint31 *)
-module Univ = Univ
-module UGraph = UGraph
-module Esubst = Esubst
-module Sorts = Sorts
-module Evar = Evar
-module Constr = Constr
-module Context = Context
-module Vars = Vars
-module Term = Term
-module Mod_subst = Mod_subst
-module Cbytecodes = Cbytecodes
-(* module Copcodes *)
-module Cemitcodes = Cemitcodes
-(* module Nativevalues *)
-(* module CPrimitives *)
-module Opaqueproof = Opaqueproof
-module Declareops = Declareops
-module Retroknowledge = Retroknowledge
-module Conv_oracle = Conv_oracle
-(* module Pre_env *)
-(* module Cbytegen *)
-(* module Nativelambda *)
-(* module Nativecode *)
-(* module Nativelib *)
-module Environ = Environ
-module CClosure = CClosure
-module Reduction = Reduction
-(* module Nativeconv *)
-module Type_errors = Type_errors
-module Modops = Modops
-module Inductive = Inductive
-module Typeops = Typeops
-(* module Indtypes *)
-(* module Cooking *)
-(* module Term_typing *)
-(* module Subtyping *)
-module Mod_typing = Mod_typing
-(* module Nativelibrary *)
-module Safe_typing = Safe_typing
-(* module Vm *)
-(* module Csymtable *)
-(* module Vconv *)
-
-(******************************************************************************)
-(* Intf *)
-(******************************************************************************)
-module Constrexpr = Constrexpr
-module Locus = Locus
-module Glob_term = Glob_term
-module Extend = Extend
-module Misctypes = Misctypes
-module Pattern = Pattern
-module Decl_kinds = Decl_kinds
-module Vernacexpr = Vernacexpr
-module Notation_term = Notation_term
-module Evar_kinds = Evar_kinds
-module Genredexpr = Genredexpr
-
-(******************************************************************************)
-(* Library *)
-(******************************************************************************)
-module Univops = Univops
-module Nameops = Nameops
-module Libnames = Libnames
-module Globnames = Globnames
-module Libobject = Libobject
-module Summary = Summary
-module Nametab = Nametab
-module Global = Global
-module Lib = Lib
-module Declaremods = Declaremods
-(* module Loadpath *)
-module Library = Library
-module States = States
-module Kindops = Kindops
-(* module Dischargedhypsmap *)
-module Goptions = Goptions
-(* module Decls *)
-(* module Heads *)
-module Keys = Keys
-module Coqlib = Coqlib
-
-(******************************************************************************)
-(* Engine *)
-(******************************************************************************)
-(* module Logic_monad *)
-module Universes = Universes
-module UState = UState
-module Evd = Evd
-module EConstr = EConstr
-module Namegen = Namegen
-module Termops = Termops
-module Proofview_monad = Proofview_monad
-module Evarutil = Evarutil
-module Proofview = Proofview
-module Ftactic = Ftactic
-module Geninterp = Geninterp
-
-(******************************************************************************)
-(* Pretyping *)
-(******************************************************************************)
-module Ltac_pretype = Ltac_pretype
-module Locusops = Locusops
-module Pretype_errors = Pretype_errors
-module Reductionops = Reductionops
-module Inductiveops = Inductiveops
-(* module Vnorm *)
-(* module Arguments_renaming *)
-module Impargs = Impargs
-(* module Nativenorm *)
-module Retyping = Retyping
-(* module Cbv *)
-module Find_subterm = Find_subterm
-(* module Evardefine *)
-module Evarsolve = Evarsolve
-module Recordops = Recordops
-module Evarconv = Evarconv
-module Typing = Typing
-module Miscops = Miscops
-module Glob_ops = Glob_ops
-module Redops = Redops
-module Patternops = Patternops
-module Constr_matching = Constr_matching
-module Tacred = Tacred
-module Typeclasses = Typeclasses
-module Classops = Classops
-(* module Program *)
-(* module Coercion *)
-module Detyping = Detyping
-module Indrec = Indrec
-(* module Cases *)
-module Pretyping = Pretyping
-module Unification = Unification
-module Univdecls = Univdecls
-(******************************************************************************)
-(* interp *)
-(******************************************************************************)
-module Tactypes = Tactypes
-module Stdarg = Stdarg
-module Genintern = Genintern
-module Constrexpr_ops = Constrexpr_ops
-module Notation_ops = Notation_ops
-module Notation = Notation
-module Dumpglob = Dumpglob
-(* module Syntax_def *)
-module Smartlocate = Smartlocate
-module Topconstr = Topconstr
-(* module Reserve *)
-(* module Implicit_quantifiers *)
-module Constrintern = Constrintern
-(* module Modintern *)
-module Constrextern = Constrextern
-(* module Discharge *)
-module Declare = Declare
-
-(******************************************************************************)
-(* Proofs *)
-(******************************************************************************)
-module Miscprint = Miscprint
-module Goal = Goal
-module Evar_refiner = Evar_refiner
-(* module Proof_using *)
-module Proof_type = Proof_type
-module Logic = Logic
-module Refine = Refine
-module Proof = Proof
-module Proof_bullet = Proof_bullet
-module Proof_global = Proof_global
-module Redexpr = Redexpr
-module Refiner = Refiner
-module Tacmach = Tacmach
-module Pfedit = Pfedit
-module Clenv = Clenv
-(* module Clenvtac *)
-(* "mli" file *)
-
-(******************************************************************************)
-(* Printing *)
-(******************************************************************************)
-module Genprint = Genprint
-module Pputils = Pputils
-module Ppconstr = Ppconstr
-module Printer = Printer
-(* module Printmod *)
-module Prettyp = Prettyp
-module Ppvernac = Ppvernac
-
-(******************************************************************************)
-(* Parsing *)
-(******************************************************************************)
-module Tok = Tok
-module CLexer = CLexer
-module Pcoq = Pcoq
-module Egramml = Egramml
-(* Egramcoq *)
-
-module G_vernac = G_vernac
-module G_proofs = G_proofs
-
-(******************************************************************************)
-(* Tactics *)
-(******************************************************************************)
-(* module Dnet *)
-(* module Dn *)
-(* module Btermdn *)
-module Tacticals = Tacticals
-module Hipattern = Hipattern
-module Ind_tables = Ind_tables
-(* module Eqschemes *)
-module Elimschemes = Elimschemes
-module Tactics = Tactics
-module Elim = Elim
-module Equality = Equality
-module Contradiction = Contradiction
-module Inv = Inv
-module Leminv = Leminv
-module Hints = Hints
-module Auto = Auto
-module Eauto = Eauto
-module Class_tactics = Class_tactics
-(* module Term_dnet *)
-module Eqdecide = Eqdecide
-module Autorewrite = Autorewrite
-
-(******************************************************************************)
-(* Vernac *)
-(******************************************************************************)
-(* module Vernacprop *)
-module Lemmas = Lemmas
-module Himsg = Himsg
-module ExplainErr = ExplainErr
-(* module Class *)
-module Locality = Locality
-module Metasyntax = Metasyntax
-(* module Auto_ind_decl *)
-module Search = Search
-(* module Indschemes *)
-module Obligations = Obligations
-module ComDefinition = ComDefinition
-module ComInductive = ComInductive
-module ComFixpoint = ComFixpoint
-module Classes = Classes
-(* module Record *)
-(* module Assumptions *)
-module Vernacstate = Vernacstate
-module Vernacinterp = Vernacinterp
-module Mltop = Mltop
-module Topfmt = Topfmt
-module Vernacentries = Vernacentries
-
-(******************************************************************************)
-(* Stm *)
-(******************************************************************************)
-module Vernac_classifier = Vernac_classifier
-module Stm = Stm
diff --git a/API/API.mli b/API/API.mli
deleted file mode 100644
index 2beebba32..000000000
--- a/API/API.mli
+++ /dev/null
@@ -1,6247 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* Warning, this file should respect the dependency order established
- in Coq. To see such order issue the comand:
-
- ```
- bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done > API/link
- ```
-
- Note however that files in intf/ are located manually now as their
- conceptual linking order in the Coq codebase is incorrect (but it
- works due to these files being implementation-free.
-
- See below in the file for their concrete position.
-*)
-
-(************************************************************************)
-(* Modules from config/ *)
-(************************************************************************)
-module Coq_config :
-sig
- val exec_extension : string
-end
-
-(************************************************************************)
-(* Modules from kernel/ *)
-(************************************************************************)
-module Names :
-sig
-
- open Util
-
- module Id :
- sig
- type t
- val equal : t -> t -> bool
- val compare : t -> t -> int
- val hash : t -> int
- val is_valid : string -> bool
- val of_bytes : bytes -> t
- val of_string : string -> t
- val of_string_soft : string -> t
- val to_string : t -> string
- val print : t -> Pp.t
-
- module Set : Set.S with type elt = t
- module Map : Map.ExtS with type key = t and module Set := Set
- module Pred : Predicate.S with type elt = t
- module List : List.MonoS with type elt = t
- val hcons : t -> t
- end
-
- module Name :
- sig
- type t = Anonymous (** anonymous identifier *)
- | Name of Id.t (** non-anonymous identifier *)
- val mk_name : Id.t -> t
- val is_anonymous : t -> bool
- val is_name : t -> bool
- val compare : t -> t -> int
- val equal : t -> t -> bool
- val hash : t -> int
- val hcons : t -> t
- val print : t -> Pp.t
- end
-
- type name = Name.t =
- | Anonymous
- | Name of Id.t
- [@@ocaml.deprecated "alias of API.Name.t"]
-
- module DirPath :
- sig
- type t
- val empty : t
- val make : Id.t list -> t
- val repr : t -> Id.t list
- val equal : t -> t -> bool
- val to_string : t -> string
- val print : t -> Pp.t
- end
-
- module MBId : sig
- type t
- val equal : t -> t -> bool
- val to_id : t -> Id.t
- val repr : t -> int * Id.t * DirPath.t
- val debug_to_string : t -> string
- end
-
- module Label :
- sig
- type t
- val make : string -> t
- val equal : t -> t -> bool
- val compare : t -> t -> int
- val of_id : Id.t -> t
- val to_id : t -> Id.t
- val to_string : t -> string
- end
-
- module ModPath :
- sig
- type t =
- | MPfile of DirPath.t
- | MPbound of MBId.t
- | MPdot of t * Label.t
- val compare : t -> t -> int
- val equal : t -> t -> bool
- val hash : t -> int
- val initial : t
- val to_string : t -> string
- val debug_to_string : t -> string
- end
-
- module KerName :
- sig
- type t
- val make : ModPath.t -> DirPath.t -> Label.t -> t
- val make2 : ModPath.t -> Label.t -> t
- val modpath : t -> ModPath.t
- val equal : t -> t -> bool
- val compare : t -> t -> int
- val label : t -> Label.t
- val repr : t -> ModPath.t * DirPath.t * Label.t
- val print : t -> Pp.t
- val to_string : t -> string
- end
-
- type kernel_name = KerName.t
- [@@ocaml.deprecated "alias of API.Names.KerName.t"]
-
- module Constant :
- sig
- type t
- val equal : t -> t -> bool
- val make1 : KerName.t -> t
- val make2 : ModPath.t -> Label.t -> t
- val make3 : ModPath.t -> DirPath.t -> Label.t -> t
- val repr3 : t -> ModPath.t * DirPath.t * Label.t
- val canonical : t -> KerName.t
- val user : t -> KerName.t
- val label : t -> Label.t
- end
-
- module MutInd :
- sig
- type t
- val make1 : KerName.t -> t
- val make2 : ModPath.t -> Label.t -> t
- val equal : t -> t -> bool
- val repr3 : t -> ModPath.t * DirPath.t * Label.t
- val canonical : t -> KerName.t
- val modpath : t -> ModPath.t
- val label : t -> Label.t
- val user : t -> KerName.t
- val print : t -> Pp.t
- end
-
- module Projection :
- sig
- type t
- val make : Constant.t -> bool -> t
- val map : (Constant.t -> Constant.t) -> t -> t
- val constant : t -> Constant.t
- val equal : t -> t -> bool
- val unfolded : t -> bool
- val unfold : t -> t
- end
-
- type evaluable_global_reference =
- | EvalVarRef of Id.t
- | EvalConstRef of Constant.t
-
- type inductive = MutInd.t * int
- val eq_ind : inductive -> inductive -> bool
-
- type constructor = inductive * int
- val eq_constructor : constructor -> constructor -> bool
- val constructor_hash : constructor -> int
-
- module MPset : Set.S with type elt = ModPath.t
- module MPmap : Map.ExtS with type key = ModPath.t and module Set := MPset
-
- module KNset : CSig.SetS with type elt = KerName.t
- module KNpred : Predicate.S with type elt = KerName.t
- module KNmap : Map.ExtS with type key = KerName.t and module Set := KNset
-
- module Cpred : Predicate.S with type elt = Constant.t
- module Cset : CSig.SetS with type elt = Constant.t
- module Cset_env : CSig.SetS with type elt = Constant.t
-
- module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset
- module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env
-
- module Mindset : CSig.SetS with type elt = MutInd.t
- module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset
- module Mindmap_env : CSig.MapS with type key = MutInd.t
-
- module Indmap : CSig.MapS with type key = inductive
- module Constrmap : CSig.MapS with type key = constructor
- module Indmap_env : CSig.MapS with type key = inductive
- module Constrmap_env : CSig.MapS with type key = constructor
-
- type transparent_state = Id.Pred.t * Cpred.t
-
- val empty_transparent_state : transparent_state
- val full_transparent_state : transparent_state
- val var_full_transparent_state : transparent_state
- val cst_full_transparent_state : transparent_state
-
- val pr_kn : KerName.t -> Pp.t
- [@@ocaml.deprecated "alias of API.Names.KerName.print"]
-
- val eq_constant : Constant.t -> Constant.t -> bool
- [@@ocaml.deprecated "alias of API.Names.Constant.equal"]
-
- type module_path = ModPath.t =
- | MPfile of DirPath.t
- | MPbound of MBId.t
- | MPdot of ModPath.t * Label.t
- [@@ocaml.deprecated "alias of API.Names.ModPath.t"]
-
- type variable = Id.t
-
- type 'a tableKey =
- | ConstKey of 'a
- | VarKey of Id.t
- | RelKey of Int.t
-
- val id_of_string : string -> Id.t
- [@@ocaml.deprecated "alias of API.Names.Id.of_string"]
-
- val string_of_id : Id.t -> string
- [@@ocaml.deprecated "alias of API.Names.Id.to_string"]
-
- type mutual_inductive = MutInd.t
- [@@ocaml.deprecated "alias of API.Names.MutInd.t"]
-
- val eq_mind : MutInd.t -> MutInd.t -> bool
- [@@ocaml.deprecated "alias of API.Names.MutInd.equal"]
-
- val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t
- [@@ocaml.deprecated "alias of API.Names.Constant.repr3"]
-
- val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t
- [@@ocaml.deprecated "alias of API.Names.MutInd.repr3"]
-
- val initial_path : ModPath.t
- [@@ocaml.deprecated "alias of API.Names.ModPath.initial"]
-
- val con_label : Constant.t -> Label.t
- [@@ocaml.deprecated "alias of API.Names.Constant.label"]
-
- val mind_label : MutInd.t -> Label.t
- [@@ocaml.deprecated "alias of API.Names.MutInd.label"]
-
- val string_of_mp : ModPath.t -> string
- [@@ocaml.deprecated "alias of API.Names.ModPath.to_string"]
-
- val mind_of_kn : KerName.t -> MutInd.t
- [@@ocaml.deprecated "alias of API.Names.MutInd.make1"]
-
- type constant = Constant.t
- [@@ocaml.deprecated "alias of API.Names.Constant.t"]
-
- val mind_modpath : MutInd.t -> ModPath.t
- [@@ocaml.deprecated "alias of API.Names.MutInd.modpath"]
-
- val canonical_mind : MutInd.t -> KerName.t
- [@@ocaml.deprecated "alias of API.Names.MutInd.canonical"]
-
- val user_mind : MutInd.t -> KerName.t
- [@@ocaml.deprecated "alias of API.Names.MutInd.user"]
-
- val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t
- [@@ocaml.deprecated "alias of API.Names.KerName.repr"]
-
- val constant_of_kn : KerName.t -> Constant.t
- [@@ocaml.deprecated "alias of API.Names.Constant.make1"]
-
- val user_con : Constant.t -> KerName.t
- [@@ocaml.deprecated "alias of API.Names.Constant.user"]
-
- val modpath : KerName.t -> ModPath.t
- [@@ocaml.deprecated "alias of API.Names.KerName.modpath"]
-
- val canonical_con : Constant.t -> KerName.t
- [@@ocaml.deprecated "alias of API.Names.Constant.canonical"]
-
- val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t
- [@@ocaml.deprecated "alias of API.Names.KerName.make"]
-
- val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t
- [@@ocaml.deprecated "alias of API.Names.Constant.make3"]
-
- val debug_pr_con : Constant.t -> Pp.t
- [@@ocaml.deprecated "Alias of Names"]
-
- val debug_pr_mind : MutInd.t -> Pp.t
- [@@ocaml.deprecated "Alias of Names"]
-
- val pr_con : Constant.t -> Pp.t
- [@@ocaml.deprecated "Alias of Names"]
-
- val string_of_con : Constant.t -> string
- [@@ocaml.deprecated "Alias of Names"]
-
- val string_of_mind : MutInd.t -> string
- [@@ocaml.deprecated "Alias of Names"]
-
- val debug_string_of_mind : MutInd.t -> string
- [@@ocaml.deprecated "Alias of Names"]
-
- val debug_string_of_con : Constant.t -> string
- [@@ocaml.deprecated "Alias of Names"]
-
- type identifier = Id.t
- [@@ocaml.deprecated "Alias of Names"]
-
- module Idset : Set.S with type elt = Id.t and type t = Id.Set.t
- [@@ocaml.deprecated "Alias of Id.Set.t"]
-
-end
-
-module Univ :
-sig
-
- module Level :
- sig
- type t
- val set : t
- val pr : t -> Pp.t
- end
-
- type universe_level = Level.t
- [@@ocaml.deprecated "Deprecated form, see univ.ml"]
-
- module LSet :
- sig
- include CSig.SetS with type elt = Level.t
- val pr : (Level.t -> Pp.t) -> t -> Pp.t
- end
-
- module Universe :
- sig
- type t
- val pr : t -> Pp.t
- end
-
- type universe = Universe.t
- [@@ocaml.deprecated "Deprecated form, see univ.ml"]
-
- module Instance :
- sig
- type t
- val empty : t
- val of_array : Level.t array -> t
- val to_array : t -> Level.t array
- val pr : (Level.t -> Pp.t) -> t -> Pp.t
- end
-
- type 'a puniverses = 'a * Instance.t
-
- val out_punivs : 'a puniverses -> 'a
-
- type constraint_type = Lt | Le | Eq
-
- type univ_constraint = Level.t * constraint_type * Level.t
-
- module Constraint : sig
- include Set.S with type elt = univ_constraint
- end
-
- type 'a constrained = 'a * Constraint.t
-
- module UContext :
- sig
- type t
- val empty : t
- end
-
- type universe_context = UContext.t
- [@@ocaml.deprecated "Deprecated form, see univ.ml"]
-
- module AUContext :
- sig
- type t
- val empty : t
- end
-
- type abstract_universe_context = AUContext.t
- [@@ocaml.deprecated "Deprecated form, see univ.ml"]
-
- module CumulativityInfo :
- sig
- type t
- end
-
- type cumulativity_info = CumulativityInfo.t
- [@@ocaml.deprecated "Deprecated form, see univ.ml"]
-
- module ACumulativityInfo :
- sig
- type t
- end
- type abstract_cumulativity_info = ACumulativityInfo.t
- [@@ocaml.deprecated "Deprecated form, see univ.ml"]
-
- module ContextSet :
- sig
- type t
- val empty : t
- val of_context : UContext.t -> t
- val to_context : t -> UContext.t
- end
-
- type 'a in_universe_context_set = 'a * ContextSet.t
- type 'a in_universe_context = 'a * UContext.t
-
- type universe_context_set = ContextSet.t
- [@@ocaml.deprecated "Deprecated form, see univ.ml"]
-
- type universe_set = LSet.t
- [@@ocaml.deprecated "Deprecated form, see univ.ml"]
-
- type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t
-
- module LMap :
- sig
- include CMap.ExtS with type key = Level.t and module Set := LSet
-
- val union : 'a t -> 'a t -> 'a t
- val diff : 'a t -> 'a t -> 'a t
- val subst_union : 'a option t -> 'a option t -> 'a option t
- val pr : ('a -> Pp.t) -> 'a t -> Pp.t
- end
-
- type 'a universe_map = 'a LMap.t
- type universe_subst = Universe.t universe_map
- type universe_level_subst = Level.t universe_map
-
- val enforce_leq : Universe.t constraint_function
- val pr_uni : Universe.t -> Pp.t
- val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t
- val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
- val pr_universe_subst : universe_subst -> Pp.t
- val pr_universe_level_subst : universe_level_subst -> Pp.t
- val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t
-end
-
-module UGraph :
-sig
- type t
- val pr_universes : (Univ.Level.t -> Pp.t) -> t -> Pp.t
-end
-
-module Esubst :
-sig
- type 'a subs
- val subs_id : int -> 'a subs
-end
-
-module Sorts :
-sig
- type contents = Pos | Null
- type t =
- | Prop of contents
- | Type of Univ.Universe.t
- val is_prop : t -> bool
- val hash : t -> int
-
- type family = InProp | InSet | InType
- val family : t -> family
- val univ_of_sort : t -> Univ.Universe.t
-end
-
-module Evar :
-sig
- (** Unique identifier of some {i evar} *)
- type t
-
- (** Recover the underlying integer. *)
- val repr : t -> int
-
- val equal : t -> t -> bool
-
- val print : t -> Pp.t
-
- (** a set of unique identifiers of some {i evars} *)
- module Set : Set.S with type elt = t
- module Map : CMap.ExtS with type key = t and module Set := Set
-
-end
-
-module Constr :
-sig
-
- open Names
-
- type t
-
- type constr = t
- type types = t
-
- type cast_kind =
- | VMcast
- | NATIVEcast
- | DEFAULTcast
- | REVERTcast
-
- type metavariable = int
-
- type existential_key = Evar.t
- [@@ocaml.deprecated "use Evar.t"]
-
- type 'constr pexistential = Evar.t * 'constr array
-
- type 'a puniverses = 'a Univ.puniverses
- [@@ocaml.deprecated "use Univ.puniverses"]
-
- type pconstant = Constant.t Univ.puniverses
- type pinductive = inductive Univ.puniverses
- type pconstructor = constructor Univ.puniverses
-
- type ('constr, 'types) prec_declaration =
- Name.t array * 'types array * 'constr array
-
- type ('constr, 'types) pfixpoint =
- (int array * int) * ('constr, 'types) prec_declaration
-
- type ('constr, 'types) pcofixpoint =
- int * ('constr, 'types) prec_declaration
-
- type case_style =
- LetStyle | IfStyle | LetPatternStyle | MatchStyle
- | RegularStyle (** infer printing form from number of constructor *)
-
- type case_printing =
- { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
- cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *)
- style : case_style }
-
- type case_info =
- { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *)
- ci_npar : int; (* number of parameters of the above inductive type *)
- ci_cstr_ndecls : int array; (* For each constructor, the corresponding integer determines
- the number of values that can be bound in a match-construct.
- NOTE: parameters of the inductive type are therefore excluded from the count *)
- ci_cstr_nargs : int array; (* for each constructor, the corresponding integers determines
- the number of values that can be applied to the constructor,
- in addition to the parameters of the related inductive type
- NOTE: "lets" are therefore excluded from the count
- NOTE: parameters of the inductive type are also excluded from the count *)
- ci_pp_info : case_printing (* not interpreted by the kernel *)
- }
-
- type ('constr, 'types, 'sort, 'univs) kind_of_term =
- | Rel of int
- | Var of Id.t
- | Meta of metavariable
- | Evar of 'constr pexistential
- | Sort of 'sort
- | Cast of 'constr * cast_kind * 'types
- | Prod of Name.t * 'types * 'types
- | Lambda of Name.t * 'types * 'constr
- | LetIn of Name.t * 'constr * 'types * 'constr
- | App of 'constr * 'constr array
- | Const of (Constant.t * 'univs)
- | Ind of (inductive * 'univs)
- | Construct of (constructor * 'univs)
- | Case of case_info * 'constr * 'constr * 'constr array
- | Fix of ('constr, 'types) pfixpoint
- | CoFix of ('constr, 'types) pcofixpoint
- | Proj of Projection.t * 'constr
-
- val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
- val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr
-
- val map_with_binders :
- ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
- val map : (constr -> constr) -> constr -> constr
-
- val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
- val iter : (constr -> unit) -> constr -> unit
- val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
-
- val equal : t -> t -> bool
- val eq_constr_nounivs : t -> t -> bool
- val compare : t -> t -> int
-
- val hash : t -> int
-
- val mkRel : int -> t
- val mkVar : Id.t -> t
- val mkMeta : metavariable -> t
- type existential = Evar.t * constr array
- val mkEvar : existential -> t
- val mkSort : Sorts.t -> t
- val mkProp : t
- val mkSet : t
- val mkType : Univ.Universe.t -> t
- val mkCast : t * cast_kind * t -> t
- val mkProd : Name.t * types * types -> types
- val mkLambda : Name.t * types * t -> t
- val mkLetIn : Name.t * t * types * t -> t
- val mkApp : t * t array -> t
- val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses
-
- type rec_declaration = Name.t array * types array * constr array
- type fixpoint = (int array * int) * rec_declaration
- val mkFix : fixpoint -> constr
-
- val mkConst : Constant.t -> t
- val mkConstU : pconstant -> t
-
- val mkProj : (Projection.t * t) -> t
-
- val mkInd : inductive -> t
- val mkIndU : pinductive -> t
-
- val mkConstruct : constructor -> t
- val mkConstructU : pconstructor -> t
- val mkConstructUi : pinductive * int -> t
-
- val mkCase : case_info * t * t * t array -> t
-
- (** {6 Simple case analysis} *)
- val isRel : constr -> bool
- val isRelN : int -> constr -> bool
- val isVar : constr -> bool
- val isVarId : Id.t -> constr -> bool
- val isInd : constr -> bool
- val isEvar : constr -> bool
- val isMeta : constr -> bool
- val isEvar_or_Meta : constr -> bool
- val isSort : constr -> bool
- val isCast : constr -> bool
- val isApp : constr -> bool
- val isLambda : constr -> bool
- val isLetIn : constr -> bool
- val isProd : constr -> bool
- val isConst : constr -> bool
- val isConstruct : constr -> bool
- val isFix : constr -> bool
- val isCoFix : constr -> bool
- val isCase : constr -> bool
- val isProj : constr -> bool
-
- val is_Prop : constr -> bool
- val is_Set : constr -> bool
- val isprop : constr -> bool
- val is_Type : constr -> bool
- val iskind : constr -> bool
- val is_small : Sorts.t -> bool
-
- (** {6 Term destructors } *)
- (** Destructor operations are partial functions and
- @raise DestKO if the term has not the expected form. *)
-
- exception DestKO
-
- (** Destructs a de Bruijn index *)
- val destRel : constr -> int
-
- (** Destructs an existential variable *)
- val destMeta : constr -> metavariable
-
- (** Destructs a variable *)
- val destVar : constr -> Id.t
-
- (** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether
- [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *)
- val destSort : constr -> Sorts.t
-
- (** Destructs a casted term *)
- val destCast : constr -> constr * cast_kind * constr
-
- (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *)
- val destProd : types -> Name.t * types * types
-
- (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
- val destLambda : constr -> Name.t * types * constr
-
- (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)
- val destLetIn : constr -> Name.t * constr * types * constr
-
- (** Destructs an application *)
- val destApp : constr -> constr * constr array
-
- (** Decompose any term as an applicative term; the list of args can be empty *)
- val decompose_app : constr -> constr * constr list
-
- (** Same as [decompose_app], but returns an array. *)
- val decompose_appvect : constr -> constr * constr array
-
- (** Destructs a constant *)
- val destConst : constr -> Constant.t Univ.puniverses
-
- (** Destructs an existential variable *)
- val destEvar : constr -> existential
-
- (** Destructs a (co)inductive type *)
- val destInd : constr -> inductive Univ.puniverses
-
- (** Destructs a constructor *)
- val destConstruct : constr -> constructor Univ.puniverses
-
- (** Destructs a [match c as x in I args return P with ... |
- Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
- return P in t1], or [if c then t1 else t2])
- @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])]
- where [info] is pretty-printing information *)
- val destCase : constr -> case_info * constr * constr * constr array
-
- (** Destructs a projection *)
- val destProj : constr -> Projection.t * constr
-
- (** Destructs the {% $ %}i{% $ %}th function of the block
- [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
- with f{_ 2} ctx{_ 2} = b{_ 2}
- ...
- with f{_ n} ctx{_ n} = b{_ n}],
- where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
- *)
- val destFix : constr -> fixpoint
-
- type cofixpoint = int * rec_declaration
- val destCoFix : constr -> cofixpoint
-
-end
-
-module Context :
-sig
- module Rel :
- sig
- module Declaration :
- sig
- (* local declaration *)
- (* local declaration *)
- type ('constr, 'types) pt =
- | LocalAssum of Names.Name.t * 'types (** name, type *)
- | LocalDef of Names.Name.t * 'constr * 'types (** name, value, type *)
-
- type t = (Constr.constr, Constr.types) pt
-
- (** Return the name bound by a given declaration. *)
- val get_name : ('c, 't) pt -> Names.Name.t
-
- (** Return the type of the name bound by a given declaration. *)
- val get_type : ('c, 't) pt -> 't
-
- (** Set the name that is bound by a given declaration. *)
- val set_name : Names.Name.t -> ('c, 't) pt -> ('c, 't) pt
-
- (** Set the type of the bound variable in a given declaration. *)
- val set_type : 't -> ('c, 't) pt -> ('c, 't) pt
-
- (** Return [true] iff a given declaration is a local assumption. *)
- val is_local_assum : ('c, 't) pt -> bool
-
- (** Return [true] iff a given declaration is a local definition. *)
- val is_local_def : ('c, 't) pt -> bool
-
- (** Check whether the two given declarations are equal. *)
- val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
-
- (** Map the name bound by a given declaration. *)
- val map_name : (Names.Name.t -> Names.Name.t) -> ('c, 't) pt -> ('c, 't) pt
-
- (** For local assumptions, this function returns the original local assumptions.
- For local definitions, this function maps the value in the local definition. *)
- val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt
-
- (** Map the type of the name bound by a given declaration. *)
- val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt
-
- (** Map all terms in a given declaration. *)
- val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
-
- (** Perform a given action on all terms in a given declaration. *)
- val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit
-
- (** Reduce all terms in a given declaration to a single value. *)
- val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a
- end
-
- (** Rel-context is represented as a list of declarations.
- Inner-most declarations are at the beginning of the list.
- Outer-most declarations are at the end of the list. *)
- type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
- type t = Declaration.t list
-
- (** empty rel-context *)
- val empty : ('c, 't) pt
-
- (** Return a new rel-context enriched by with a given inner-most declaration. *)
- val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
-
- (** Return the number of {e local declarations} in a given context. *)
- val length : ('c, 't) pt -> int
-
- (** Check whether given two rel-contexts are equal. *)
- val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
-
- (** Return the number of {e local assumptions} in a given rel-context. *)
- val nhyps : ('c, 't) pt -> int
-
- (** Return a declaration designated by a given de Bruijn index.
- @raise Not_found if the designated de Bruijn index outside the range. *)
- val lookup : int -> ('c, 't) pt -> ('c, 't) Declaration.pt
-
- (** Map all terms in a given rel-context. *)
- val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
-
- (** Perform a given action on every declaration in a given rel-context. *)
- val iter : ('c -> unit) -> ('c, 'c) pt -> unit
-
- (** Reduce all terms in a given rel-context to a single value.
- Innermost declarations are processed first. *)
- val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a
-
- (** Reduce all terms in a given rel-context to a single value.
- Outermost declarations are processed first. *)
- val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a
-
- (** [extended_vect n Γ] does the same, returning instead an array. *)
- val to_extended_vect : (int -> 'r) -> int -> ('c, 't) pt -> 'r array
- end
- module Named :
- sig
- module Declaration :
- sig
- (** local declaration *)
- type ('constr, 'types) pt =
- | LocalAssum of Names.Id.t * 'types (** identifier, type *)
- | LocalDef of Names.Id.t * 'constr * 'types (** identifier, value, type *)
-
- type t = (Constr.constr, Constr.types) pt
-
- (** Return the identifier bound by a given declaration. *)
- val get_id : ('c, 't) pt -> Names.Id.t
-
- (** Return the type of the name bound by a given declaration. *)
- val get_type : ('c, 't) pt -> 't
-
- (** Set the identifier that is bound by a given declaration. *)
- val set_id : Names.Id.t -> ('c, 't) pt -> ('c, 't) pt
-
- (** Set the type of the bound variable in a given declaration. *)
- val set_type : 't -> ('c, 't) pt -> ('c, 't) pt
-
- (** Return [true] iff a given declaration is a local assumption. *)
- val is_local_assum : ('c, 't) pt -> bool
-
- (** Return [true] iff a given declaration is a local definition. *)
- val is_local_def : ('c, 't) pt -> bool
-
- (** Check whether any term in a given declaration satisfies a given predicate. *)
- val exists : ('c -> bool) -> ('c, 'c) pt -> bool
-
- (** Check whether all terms in a given declaration satisfy a given predicate. *)
- val for_all : ('c -> bool) -> ('c, 'c) pt -> bool
-
- (** Check whether the two given declarations are equal. *)
- val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
-
- (** Map the identifier bound by a given declaration. *)
- val map_id : (Names.Id.t -> Names.Id.t) -> ('c, 't) pt -> ('c, 't) pt
-
- (** For local assumptions, this function returns the original local assumptions.
- For local definitions, this function maps the value in the local definition. *)
- val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt
-
- (** Map the type of the name bound by a given declaration. *)
- val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt
-
- (** Map all terms in a given declaration. *)
- val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
-
- (** Perform a given action on all terms in a given declaration. *)
- val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit
-
- (** Reduce all terms in a given declaration to a single value. *)
- val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a
-
- val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt
- end
- (** Named-context is represented as a list of declarations.
- Inner-most declarations are at the beginning of the list.
- Outer-most declarations are at the end of the list. *)
- type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
- type t = Declaration.t list
-
- (** empty named-context *)
- val empty : ('c, 't) pt
-
- (** Return a new named-context enriched by with a given inner-most declaration. *)
- val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
-
- (** Return the number of {e local declarations} in a given named-context. *)
- val length : ('c, 't) pt -> int
-
- (** Return a declaration designated by an identifier of the variable bound in that declaration.
- @raise Not_found if the designated identifier is not bound in a given named-context. *)
- val lookup : Names.Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt
-
- (** Check whether given two named-contexts are equal. *)
- val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
-
- (** Map all terms in a given named-context. *)
- val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
-
- (** Perform a given action on every declaration in a given named-context. *)
- val iter : ('c -> unit) -> ('c, 'c) pt -> unit
-
- (** Reduce all terms in a given named-context to a single value.
- Innermost declarations are processed first. *)
- val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a
-
- (** Reduce all terms in a given named-context to a single value.
- Outermost declarations are processed first. *)
- val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a
-
- (** Return the set of all identifiers bound in a given named-context. *)
- val to_vars : ('c, 't) pt -> Names.Id.Set.t
-
- (** [to_instance Ω] builds an instance [args] such
- that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local
- definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
- gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
- val to_instance : (Names.Id.t -> 'r) -> ('c, 't) pt -> 'r list
- end
-end
-
-module Vars :
-sig
- type substl = Constr.t list
-
- val substl : substl -> Constr.t -> Constr.t
-
- val subst1 : Constr.t -> Constr.t -> Constr.t
-
- val lift : int -> Constr.t -> Constr.t
-
- val closed0 : Constr.t -> bool
-
- val closedn : int -> Constr.t -> bool
-
- val replace_vars : (Names.Id.t * Constr.t) list -> Constr.t -> Constr.t
-
- val noccurn : int -> Constr.t -> bool
- val subst_var : Names.Id.t -> Constr.t -> Constr.t
- val subst_vars : Names.Id.t list -> Constr.t -> Constr.t
- val substnl : substl -> int -> Constr.t -> Constr.t
-end
-
-module Term :
-sig
-
- open Constr
- type sorts_family = Sorts.family = InProp | InSet | InType
- [@@ocaml.deprecated "Alias of Sorts.family"]
-
- type contents = Sorts.contents = Pos | Null
- [@@ocaml.deprecated "Alias of Sorts.contents"]
-
- type sorts = Sorts.t =
- | Prop of Sorts.contents
- | Type of Univ.Universe.t
- [@@ocaml.deprecated "alias of API.Sorts.t"]
-
- type metavariable = int
- [@@ocaml.deprecated "Alias of Constr.metavariable"]
-
- type ('constr, 'types) prec_declaration = Names.Name.t array * 'types array * 'constr array
- [@@ocaml.deprecated "Alias of Constr.prec_declaration"]
-
- type 'constr pexistential = 'constr Constr.pexistential
- [@@ocaml.deprecated "Alias of Constr.pexistential"]
-
- type cast_kind = Constr.cast_kind =
- | VMcast
- | NATIVEcast
- | DEFAULTcast
- | REVERTcast
- [@@ocaml.deprecated "Alias of Constr.cast_kind"]
-
- type 'a puniverses = 'a Univ.puniverses
- [@@ocaml.deprecated "Alias of Constr.puniverses"]
- type pconstant = Names.Constant.t Univ.puniverses
- [@@ocaml.deprecated "Alias of Constr.pconstant"]
- type pinductive = Names.inductive Univ.puniverses
- [@@ocaml.deprecated "Alias of Constr.pinductive"]
- type pconstructor = Names.constructor Univ.puniverses
- [@@ocaml.deprecated "Alias of Constr.pconstructor"]
- type case_style = Constr.case_style =
- | LetStyle
- | IfStyle
- | LetPatternStyle
- | MatchStyle
- | RegularStyle
- [@@ocaml.deprecated "Alias of Constr.case_style"]
-
- type case_printing = Constr.case_printing =
- { ind_tags : bool list;
- cstr_tags : bool list array;
- style : Constr.case_style
- }
- [@@ocaml.deprecated "Alias of Constr.case_printing"]
-
- type case_info = Constr.case_info =
- { ci_ind : Names.inductive;
- ci_npar : int;
- ci_cstr_ndecls: int array;
- ci_cstr_nargs : int array;
- ci_pp_info : Constr.case_printing
- }
- [@@ocaml.deprecated "Alias of Constr.case_info"]
-
- type ('constr, 'types) pfixpoint =
- (int array * int) * ('constr, 'types) Constr.prec_declaration
- [@@ocaml.deprecated "Alias of Constr.pfixpoint"]
-
- type ('constr, 'types) pcofixpoint =
- int * ('constr, 'types) Constr.prec_declaration
- [@@ocaml.deprecated "Alias of Constr.pcofixpoint"]
-
- type ('constr, 'types, 'sort, 'univs) kind_of_term = ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
- | Rel of int
- | Var of Names.Id.t
- | Meta of Constr.metavariable
- | Evar of 'constr Constr.pexistential
- | Sort of 'sort
- | Cast of 'constr * Constr.cast_kind * 'types
- | Prod of Names.Name.t * 'types * 'types
- | Lambda of Names.Name.t * 'types * 'constr
- | LetIn of Names.Name.t * 'constr * 'types * 'constr
- | App of 'constr * 'constr array
- | Const of (Names.Constant.t * 'univs)
- | Ind of (Names.inductive * 'univs)
- | Construct of (Names.constructor * 'univs)
- | Case of Constr.case_info * 'constr * 'constr * 'constr array
- | Fix of ('constr, 'types) Constr.pfixpoint
- | CoFix of ('constr, 'types) Constr.pcofixpoint
- | Proj of Names.Projection.t * 'constr
- [@@ocaml.deprecated "Alias of Constr.kind_of_term"]
- type existential = Evar.t * Constr.constr array
- [@@ocaml.deprecated "Alias of Constr.existential"]
- type rec_declaration = Names.Name.t array * Constr.constr array * Constr.constr array
- [@@ocaml.deprecated "Alias of Constr.rec_declaration"]
- val kind_of_term : Constr.constr -> (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
- [@@ocaml.deprecated "Alias of Constr.kind"]
- val applistc : Constr.constr -> Constr.constr list -> Constr.constr
-
- val applist : constr * constr list -> constr
- [@@ocaml.deprecated "(sort of an) alias of API.Term.applistc"]
-
- val mkArrow : types -> types -> constr
- val mkRel : int -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkVar : Names.Id.t -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
-
- val mkMeta : Constr.metavariable -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
-
- val mkEvar : Constr.existential -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkSort : Sorts.t -> types
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkProp : types
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkSet : types
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkType : Univ.Universe.t -> types
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkCast : constr * Constr.cast_kind * constr -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkProd : Names.Name.t * types * types -> types
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkLambda : Names.Name.t * types * constr -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkLetIn : Names.Name.t * constr * types * constr -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkApp : constr * constr array -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkConst : Names.Constant.t -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkProj : Names.Projection.t * constr -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkInd : Names.inductive -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkConstruct : Names.constructor -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkConstructU : Names.constructor Univ.puniverses -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkConstructUi : (Constr.pinductive * int) -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkCase : Constr.case_info * constr * constr * constr array -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkFix : fixpoint -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
- val mkCoFix : cofixpoint -> constr
- [@@ocaml.deprecated "Alias of similarly named Constr function"]
-
- val mkNamedLambda : Names.Id.t -> types -> constr -> constr
- val mkNamedLetIn : Names.Id.t -> constr -> types -> constr -> constr
- val mkNamedProd : Names.Id.t -> types -> types -> types
-
- val decompose_app : constr -> constr * constr list
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
-
- val decompose_prod : constr -> (Names.Name.t*constr) list * constr
- val decompose_prod_n : int -> constr -> (Names.Name.t * constr) list * constr
- val decompose_prod_assum : types -> Context.Rel.t * types
- val decompose_lam : constr -> (Names.Name.t * constr) list * constr
- val decompose_lam_n : int -> constr -> (Names.Name.t * constr) list * constr
- val decompose_prod_n_assum : int -> types -> Context.Rel.t * types
-
- val compose_prod : (Names.Name.t * constr) list -> constr -> constr
- val compose_lam : (Names.Name.t * constr) list -> constr -> constr
-
- val destSort : constr -> Sorts.t
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val destVar : constr -> Names.Id.t
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val destApp : constr -> constr * constr array
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val destProd : types -> Names.Name.t * types * types
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val destLetIn : constr -> Names.Name.t * constr * types * constr
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val destEvar : constr -> Constr.existential
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val destRel : constr -> int
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val destConst : constr -> Names.Constant.t Univ.puniverses
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val destCast : constr -> constr * Constr.cast_kind * constr
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val destLambda : constr -> Names.Name.t * types * constr
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
-
- val isRel : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val isVar : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val isEvar : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val isLetIn : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val isLambda : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val isConst : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val isEvar_or_Meta : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val isCast : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val isMeta : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val isApp : constr -> bool
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
-
- val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
- [@@ocaml.deprecated "Alias of Constr.fold"]
-
- val eq_constr : constr -> constr -> bool
- [@@ocaml.deprecated "Alias of Constr.equal"]
-
- val hash_constr : constr -> int
- [@@ocaml.deprecated "Alias of Constr.hash"]
-
- val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
- val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
- val prod_applist : constr -> constr list -> constr
-
- val map_constr : (constr -> constr) -> constr -> constr
- [@@ocaml.deprecated "Alias of Constr.map"]
-
- val mkIndU : Constr.pinductive -> constr
- [@@ocaml.deprecated "Alias of Constr.mkIndU"]
- val mkConstU : Constr.pconstant -> constr
- [@@ocaml.deprecated "Alias of Constr.mkConstU"]
- val map_constr_with_binders :
- ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
- [@@ocaml.deprecated "Alias of Constr.map_with_binders"]
-
- val iter_constr : (constr -> unit) -> constr -> unit
- [@@ocaml.deprecated "Alias of Constr.iter."]
-
- (* Quotients away universes: really needed?
- * Can't we just call eq_c_univs_infer and discard the inferred csts?
- *)
- val eq_constr_nounivs : constr -> constr -> bool
- [@@ocaml.deprecated "Alias of Constr.qe_constr_nounivs."]
-
- type ('constr, 'types) kind_of_type =
- | SortType of Sorts.t
- | CastType of 'types * 'types
- | ProdType of Names.Name.t * 'types * 'types
- | LetInType of Names.Name.t * 'constr * 'types * 'types
- | AtomicType of 'constr * 'constr array
-
- val kind_of_type : types -> (constr, types) kind_of_type
-
- val is_prop_sort : Sorts.t -> bool
- [@@ocaml.deprecated "alias of API.Sorts.is_prop"]
-
- type existential_key = Evar.t
- [@@ocaml.deprecated "Alias of Constr.existential_key"]
-
- val family_of_sort : Sorts.t -> Sorts.family
- [@@ocaml.deprecated "Alias of Sorts.family"]
-
- val compare : constr -> constr -> int
- [@@ocaml.deprecated "Alias of Constr.compare."]
-
- val constr_ord : constr -> constr -> int
- [@@ocaml.deprecated "alias of Term.compare"]
-
- val destInd : constr -> Names.inductive Univ.puniverses
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
- val univ_of_sort : Sorts.t -> Univ.Universe.t
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
-
- val strip_lam : constr -> constr
- val strip_prod_assum : types -> types
-
- val decompose_lam_assum : constr -> Context.Rel.t * constr
- val destFix : constr -> fixpoint
- [@@ocaml.deprecated "Alias for the function in [Constr]"]
-
- val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
- [@@ocaml.deprecated "Alias of Constr.compare_head."]
-
- type constr = Constr.t
- [@@ocaml.deprecated "Alias of Constr.t"]
- type types = Constr.t
- [@@ocaml.deprecated "Alias of Constr.types"]
-
- type fixpoint = (int array * int) * Constr.rec_declaration
- [@@ocaml.deprecated "Alias of Constr.Constr.fixpoint"]
- type cofixpoint = int * Constr.rec_declaration
- [@@ocaml.deprecated "Alias of Constr.cofixpoint"]
-
-end
-
-module Mod_subst :
-sig
- type delta_resolver
- type substitution
- type 'a substituted
-
- val force_constr : Constr.t substituted -> Constr.t
-
- val empty_delta_resolver : delta_resolver
- val constant_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.Constant.t
- val mind_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.MutInd.t
- val subst_kn : substitution -> Names.KerName.t -> Names.KerName.t
- val subst_evaluable_reference :
- substitution -> Names.evaluable_global_reference -> Names.evaluable_global_reference
- val subst_mps : substitution -> Constr.t -> Constr.t
- val subst_constant : substitution -> Names.Constant.t -> Names.Constant.t
- val subst_ind : substitution -> Names.inductive -> Names.inductive
- val debug_pr_subst : substitution -> Pp.t
- val debug_pr_delta : delta_resolver -> Pp.t
-end
-
-module Opaqueproof :
-sig
- type opaquetab
- type opaque
- val empty_opaquetab : opaquetab
- val force_proof : opaquetab -> opaque -> Constr.t
-end
-
-module Cbytecodes :
-sig
- type tag = int
- type reloc_table = (tag * int) array
-end
-
-module Cemitcodes :
-sig
- type to_patch_substituted
-end
-
-module Retroknowledge :
-sig
- type action
- type nat_field =
- | NatType
- | NatPlus
- | NatTimes
- type n_field =
- | NPositive
- | NType
- | NTwice
- | NTwicePlusOne
- | NPhi
- | NPhiInv
- | NPlus
- | NTimes
- type int31_field =
- | Int31Bits
- | Int31Type
- | Int31Constructor
- | Int31Twice
- | Int31TwicePlusOne
- | Int31Phi
- | Int31PhiInv
- | Int31Plus
- | Int31PlusC
- | Int31PlusCarryC
- | Int31Minus
- | Int31MinusC
- | Int31MinusCarryC
- | Int31Times
- | Int31TimesC
- | Int31Div21
- | Int31Div
- | Int31Diveucl
- | Int31AddMulDiv
- | Int31Compare
- | Int31Head0
- | Int31Tail0
- | Int31Lor
- | Int31Land
- | Int31Lxor
- type field =
- | KInt31 of string * int31_field
-end
-
-module Conv_oracle :
-sig
- type level
-end
-
-module Declarations :
-sig
-
- open Names
-
- type recarg =
- | Norec
- | Mrec of Names.inductive
- | Imbr of Names.inductive
- type wf_paths = recarg Rtree.t
- type inline = int option
- type constant_def =
- | Undef of inline
- | Def of Constr.t Mod_subst.substituted
- | OpaqueDef of Opaqueproof.opaque
- type template_arity = {
- template_param_levels : Univ.Level.t option list;
- template_level : Univ.Universe.t;
- }
-
- type ('a, 'b) declaration_arity =
- | RegularArity of 'a
- | TemplateArity of 'b
-
- type constant_universes =
- | Monomorphic_const of Univ.ContextSet.t
- | Polymorphic_const of Univ.AUContext.t
-
- type projection_body = {
- proj_ind : Names.MutInd.t;
- proj_npars : int;
- proj_arg : int;
- proj_type : Constr.types;
- proj_eta : Constr.t * Constr.types;
- proj_body : Constr.t;
- }
-
- type typing_flags = {
- check_guarded : bool;
- check_universes : bool;
- }
-
- type constant_body = {
- const_hyps : Context.Named.t;
- const_body : constant_def;
- const_type : Constr.types;
- const_body_code : Cemitcodes.to_patch_substituted option;
- const_universes : constant_universes;
- const_proj : projection_body option;
- const_inline_code : bool;
- const_typing_flags : typing_flags;
- }
-
- type regular_inductive_arity = {
- mind_user_arity : Constr.types;
- mind_sort : Sorts.t;
- }
-
- type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity
-
- type one_inductive_body = {
- mind_typename : Names.Id.t;
- mind_arity_ctxt : Context.Rel.t;
- mind_arity : inductive_arity;
- mind_consnames : Names.Id.t array;
- mind_user_lc : Constr.types array;
- mind_nrealargs : int;
- mind_nrealdecls : int;
- mind_kelim : Sorts.family list;
- mind_nf_lc : Constr.types array;
- mind_consnrealargs : int array;
- mind_consnrealdecls : int array;
- mind_recargs : wf_paths;
- mind_nb_constant : int;
- mind_nb_args : int;
- mind_reloc_tbl : Cbytecodes.reloc_table;
- }
-
- type ('ty,'a) functorize =
- | NoFunctor of 'a
- | MoreFunctor of Names.MBId.t * 'ty * ('ty,'a) functorize
-
- type with_declaration =
- | WithMod of Names.Id.t list * Names.ModPath.t
- | WithDef of Names.Id.t list * Constr.t Univ.in_universe_context
-
- type module_alg_expr =
- | MEident of Names.ModPath.t
- | MEapply of module_alg_expr * Names.ModPath.t
- | MEwith of module_alg_expr * with_declaration
-
- type abstract_inductive_universes =
- | Monomorphic_ind of Univ.ContextSet.t
- | Polymorphic_ind of Univ.AUContext.t
- | Cumulative_ind of Univ.ACumulativityInfo.t
-
- type record_body = (Id.t * Constant.t array * projection_body array) option
-
- type recursivity_kind =
- | Finite (** = inductive *)
- | CoFinite (** = coinductive *)
- | BiFinite (** = non-recursive, like in "Record" definitions *)
-
- type mutual_inductive_body = {
- mind_packets : one_inductive_body array;
- mind_record : record_body option;
- mind_finite : recursivity_kind;
- mind_ntypes : int;
- mind_hyps : Context.Named.t;
- mind_nparams : int;
- mind_nparams_rec : int;
- mind_params_ctxt : Context.Rel.t;
- mind_universes : abstract_inductive_universes;
- mind_private : bool option;
- mind_typing_flags : typing_flags;
- }
- and module_expression = (module_type_body,module_alg_expr) functorize
- and module_implementation =
- | Abstract
- | Algebraic of module_expression
- | Struct of module_signature
- | FullStruct
- and 'a generic_module_body =
- { mod_mp : Names.ModPath.t;
- mod_expr : 'a;
- mod_type : module_signature;
- mod_type_alg : module_expression option;
- mod_constraints : Univ.ContextSet.t;
- mod_delta : Mod_subst.delta_resolver;
- mod_retroknowledge : 'a module_retroknowledge;
- }
- and module_signature = (module_type_body,structure_body) functorize
- and module_body = module_implementation generic_module_body
- and module_type_body = unit generic_module_body
- and structure_body = (Names.Label.t * structure_field_body) list
- and structure_field_body =
- | SFBconst of constant_body
- | SFBmind of mutual_inductive_body
- | SFBmodule of module_body
- | SFBmodtype of module_type_body
- and _ module_retroknowledge =
- | ModBodyRK :
- Retroknowledge.action list -> module_implementation module_retroknowledge
- | ModTypeRK : unit module_retroknowledge
-end
-
-module Declareops :
-sig
- val constant_has_body : Declarations.constant_body -> bool
- val is_opaque : Declarations.constant_body -> bool
- val eq_recarg : Declarations.recarg -> Declarations.recarg -> bool
-end
-
-module Entries :
-sig
-
- open Names
- open Constr
-
- type local_entry =
- | LocalDefEntry of constr
- | LocalAssumEntry of constr
-
- type inductive_universes =
- | Monomorphic_ind_entry of Univ.ContextSet.t
- | Polymorphic_ind_entry of Univ.UContext.t
- | Cumulative_ind_entry of Univ.CumulativityInfo.t
-
- type one_inductive_entry = {
- mind_entry_typename : Id.t;
- mind_entry_arity : constr;
- mind_entry_template : bool; (* Use template polymorphism *)
- mind_entry_consnames : Id.t list;
- mind_entry_lc : constr list }
-
- type mutual_inductive_entry = {
- mind_entry_record : (Names.Id.t option) option;
- (** Some (Some id): primitive record with id the binder name of the record
- in projections.
- Some None: non-primitive record *)
- mind_entry_finite : Declarations.recursivity_kind;
- mind_entry_params : (Id.t * local_entry) list;
- mind_entry_inds : one_inductive_entry list;
- mind_entry_universes : inductive_universes;
- (* universe constraints and the constraints for subtyping of
- inductive types in the block. *)
- mind_entry_private : bool option;
- }
-
- type inline = int option
- type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a
- type 'a const_entry_body = 'a proof_output Future.computation
- type constant_universes_entry =
- | Monomorphic_const_entry of Univ.ContextSet.t
- | Polymorphic_const_entry of Univ.UContext.t
- type 'a in_constant_universes_entry = 'a * constant_universes_entry
- type 'a definition_entry =
- { const_entry_body : 'a const_entry_body;
- (* List of section variables *)
- const_entry_secctx : Context.Named.t option;
- (* State id on which the completion of type checking is reported *)
- const_entry_feedback : Stateid.t option;
- const_entry_type : Constr.types option;
- const_entry_universes : constant_universes_entry;
- const_entry_opaque : bool;
- const_entry_inline_code : bool }
- type parameter_entry = Context.Named.t option * Constr.types in_constant_universes_entry * inline
-
- type projection_entry = {
- proj_entry_ind : MutInd.t;
- proj_entry_arg : int }
-
- type 'a constant_entry =
- | DefinitionEntry of 'a definition_entry
- | ParameterEntry of parameter_entry
- | ProjectionEntry of projection_entry
- type module_struct_entry = Declarations.module_alg_expr
- type module_params_entry =
- (Names.MBId.t * module_struct_entry) list
- type module_type_entry = module_params_entry * module_struct_entry
-end
-
-module Environ :
-sig
- type env
- type named_context_val
-
- type ('constr, 'types) punsafe_judgment =
- {
- uj_val : 'constr;
- uj_type : 'types
- }
- type 'types punsafe_type_judgment = {
- utj_val : 'types;
- utj_type : Sorts.t }
-
- type unsafe_type_judgment = Constr.types punsafe_type_judgment
- val empty_env : env
- val lookup_mind : Names.MutInd.t -> env -> Declarations.mutual_inductive_body
- val push_rel : Context.Rel.Declaration.t -> env -> env
- val push_rel_context : Context.Rel.t -> env -> env
- val push_rec_types : Constr.rec_declaration -> env -> env
- val lookup_rel : int -> env -> Context.Rel.Declaration.t
- val lookup_named : Names.Id.t -> env -> Context.Named.Declaration.t
- val lookup_named_val : Names.Id.t -> named_context_val -> Context.Named.Declaration.t
- val lookup_constant : Names.Constant.t -> env -> Declarations.constant_body
- val opaque_tables : env -> Opaqueproof.opaquetab
- val is_projection : Names.Constant.t -> env -> bool
- val lookup_projection : Names.Projection.t -> env -> Declarations.projection_body
- val named_context_of_val : named_context_val -> Context.Named.t
- val push_named : Context.Named.Declaration.t -> env -> env
- val named_context : env -> Context.Named.t
- val named_context_val : env -> named_context_val
- val push_named_context_val : Context.Named.Declaration.t -> named_context_val -> named_context_val
- val reset_with_named_context : named_context_val -> env -> env
- val rel_context : env -> Context.Rel.t
- val constant_value_in : env -> Names.Constant.t Univ.puniverses -> Constr.t
- val named_type : Names.Id.t -> env -> Constr.types
- val constant_opt_value_in : env -> Names.Constant.t Univ.puniverses -> Constr.t option
- val fold_named_context_reverse :
- ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a
- val evaluable_named : Names.Id.t -> env -> bool
- val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
-end
-
-module CClosure :
-sig
-
- type table_key = Names.Constant.t Univ.puniverses Names.tableKey
-
- type fconstr
-
- type fterm =
- | FRel of int
- | FAtom of Constr.t (** Metas and Sorts *)
- | FCast of fconstr * Constr.cast_kind * fconstr
- | FFlex of table_key
- | FInd of Names.inductive Univ.puniverses
- | FConstruct of Names.constructor Univ.puniverses
- | FApp of fconstr * fconstr array
- | FProj of Names.Projection.t * fconstr
- | FFix of Constr.fixpoint * fconstr Esubst.subs
- | FCoFix of Constr.cofixpoint * fconstr Esubst.subs
- | FCaseT of Constr.case_info * Constr.t * fconstr * Constr.t array * fconstr Esubst.subs (* predicate and branches are closures *)
- | FLambda of int * (Names.Name.t * Constr.t) list * Constr.t * fconstr Esubst.subs
- | FProd of Names.Name.t * fconstr * fconstr
- | FLetIn of Names.Name.t * fconstr * fconstr * Constr.t * fconstr Esubst.subs
- | FEvar of Constr.existential * fconstr Esubst.subs
- | FLIFT of int * fconstr
- | FCLOS of Constr.t * fconstr Esubst.subs
- | FLOCKED
-
- module RedFlags : sig
- type reds
- type red_kind
- val mkflags : red_kind list -> reds
- val fBETA : red_kind
- val fCOFIX : red_kind
- val fCONST : Names.Constant.t -> red_kind
- val fFIX : red_kind
- val fMATCH : red_kind
- val fZETA : red_kind
- val red_add_transparent : reds -> Names.transparent_state -> reds
- end
-
- type 'a infos_cache
- type 'a infos = {
- i_flags : RedFlags.reds;
- i_cache : 'a infos_cache }
-
- type clos_infos = fconstr infos
-
- val mk_clos : fconstr Esubst.subs -> Constr.t -> fconstr
- val mk_atom : Constr.t -> fconstr
- val mk_clos_deep :
- (fconstr Esubst.subs -> Constr.t -> fconstr) ->
- fconstr Esubst.subs -> Constr.t -> fconstr
- val mk_red : fterm -> fconstr
- val all : RedFlags.reds
- val beta : RedFlags.reds
- val betaiota : RedFlags.reds
- val betaiotazeta : RedFlags.reds
-
- val create_clos_infos : ?evars:(Constr.existential -> Constr.t option) -> RedFlags.reds -> Environ.env -> clos_infos
-
- val whd_val : clos_infos -> fconstr -> Constr.t
-
- val inject : Constr.t -> fconstr
-
- val kl : clos_infos -> fconstr -> Constr.t
- val term_of_fconstr : fconstr -> Constr.t
-end
-
-module Reduction :
-sig
- exception NotConvertible
- type conv_pb =
- | CONV
- | CUMUL
-
- val whd_all : Environ.env -> Constr.t -> Constr.t
-
- val whd_betaiotazeta : Environ.env -> Constr.t -> Constr.t
-
- val is_arity : Environ.env -> Constr.types -> bool
-
- val dest_prod : Environ.env -> Constr.types -> Context.Rel.t * Constr.types
-
- type 'a extended_conversion_function =
- ?l2r:bool -> ?reds:Names.transparent_state -> Environ.env ->
- ?evars:((Constr.existential->Constr.t option) * UGraph.t) ->
- 'a -> 'a -> unit
- val conv : Constr.t extended_conversion_function
-end
-
-module Type_errors :
-sig
-
- open Names
- open Constr
- open Environ
-
- type 'constr pguard_error =
- (** Fixpoints *)
- | NotEnoughAbstractionInFixBody
- | RecursionNotOnInductiveType of 'constr
- | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list
- | NotEnoughArgumentsForFixCall of int
- (** CoFixpoints *)
- | CodomainNotInductiveType of 'constr
- | NestedRecursiveOccurrences
- | UnguardedRecursiveCall of 'constr
- | RecCallInTypeOfAbstraction of 'constr
- | RecCallInNonRecArgOfConstructor of 'constr
- | RecCallInTypeOfDef of 'constr
- | RecCallInCaseFun of 'constr
- | RecCallInCaseArg of 'constr
- | RecCallInCasePred of 'constr
- | NotGuardedForm of 'constr
- | ReturnPredicateNotCoInductive of 'constr
-
- type arity_error =
- | NonInformativeToInformative
- | StrongEliminationOnNonSmallType
- | WrongArity
-
- type ('constr, 'types) ptype_error =
- | UnboundRel of int
- | UnboundVar of variable
- | NotAType of ('constr, 'types) punsafe_judgment
- | BadAssumption of ('constr, 'types) punsafe_judgment
- | ReferenceVariables of Id.t * 'constr
- | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment
- * (Sorts.family * Sorts.family * arity_error) option
- | CaseNotInductive of ('constr, 'types) punsafe_judgment
- | WrongCaseInfo of pinductive * case_info
- | NumberBranches of ('constr, 'types) punsafe_judgment * int
- | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
- | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
- | ActualType of ('constr, 'types) punsafe_judgment * 'types
- | CantApplyBadType of
- (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
- | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
- | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array
- | IllTypedRecBody of
- int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
- | UnsatisfiedConstraints of Univ.Constraint.t
-
- type type_error = (constr, types) ptype_error
-
- exception TypeError of Environ.env * type_error
-end
-
-module Modops :
-sig
- val destr_nofunctor : ('ty,'a) Declarations.functorize -> 'a
- val add_structure :
- Names.ModPath.t -> Declarations.structure_body -> Mod_subst.delta_resolver ->
- Environ.env -> Environ.env
- val add_module_type : Names.ModPath.t -> Declarations.module_type_body -> Environ.env -> Environ.env
-end
-
-module Inductive :
-sig
- type mind_specif = Declarations.mutual_inductive_body * Declarations.one_inductive_body
- val type_of_inductive : Environ.env -> mind_specif Univ.puniverses -> Constr.types
- exception SingletonInductiveBecomesProp of Names.Id.t
- val lookup_mind_specif : Environ.env -> Names.inductive -> mind_specif
- val find_inductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.t list
-end
-
-module Typeops :
-sig
- val infer_type : Environ.env -> Constr.types -> Environ.unsafe_type_judgment
- val type_of_constant_in : Environ.env -> Constr.pconstant -> Constr.types
-end
-
-module Mod_typing :
-sig
- type 'alg translation =
- Declarations.module_signature * 'alg * Mod_subst.delta_resolver * Univ.ContextSet.t
- val translate_modtype :
- Environ.env -> Names.ModPath.t -> Entries.inline ->
- Entries.module_type_entry -> Declarations.module_type_body
- val translate_mse :
- Environ.env -> Names.ModPath.t option -> Entries.inline -> Declarations.module_alg_expr ->
- Declarations.module_alg_expr translation
-end
-
-module Safe_typing :
-sig
- type private_constants
- val mk_pure_proof : Constr.t -> private_constants Entries.proof_output
-end
-
-(************************************************************************)
-(* End of modules from kernel/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from intf/ *)
-(************************************************************************)
-
-module Libnames :
-sig
-
- open Util
- open Names
-
- type full_path
- val pr_path : full_path -> Pp.t
- val make_path : Names.DirPath.t -> Names.Id.t -> full_path
- val eq_full_path : full_path -> full_path -> bool
- val repr_path : full_path -> Names.DirPath.t * Names.Id.t
- val dirpath : full_path -> Names.DirPath.t
- val path_of_string : string -> full_path
-
- type qualid
- val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid
- val qualid_eq : qualid -> qualid -> bool
- val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t
- val pr_qualid : qualid -> Pp.t
- val string_of_qualid : qualid -> string
- val qualid_of_string : string -> qualid
- val qualid_of_path : full_path -> qualid
- val qualid_of_dirpath : Names.DirPath.t -> qualid
- val qualid_of_ident : Names.Id.t -> qualid
-
- type reference =
- | Qualid of qualid Loc.located
- | Ident of Names.Id.t Loc.located
- val loc_of_reference : reference -> Loc.t option
- val qualid_of_reference : reference -> qualid Loc.located
- val pr_reference : reference -> Pp.t
-
- val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool
- val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t
- val dirpath_of_string : string -> Names.DirPath.t
- val pr_dirpath : Names.DirPath.t -> Pp.t
- [@@ocaml.deprecated "Alias for DirPath.print"]
-
- val string_of_path : full_path -> string
-
- val basename : full_path -> Names.Id.t
-
- type object_name = full_path * Names.KerName.t
- type object_prefix = {
- obj_dir : DirPath.t;
- obj_mp : ModPath.t;
- obj_sec : DirPath.t;
- }
-
- module Dirset : Set.S with type elt = DirPath.t
- module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
- module Spmap : CSig.MapS with type key = full_path
-end
-
-module Misctypes :
-sig
- type evars_flag = bool
- type clear_flag = bool option
- type advanced_flag = bool
- type rec_flag = bool
-
- type 'a or_by_notation =
- | AN of 'a
- | ByNotation of (string * string option) Loc.located
-
- type 'a or_var =
- | ArgArg of 'a
- | ArgVar of Names.Id.t Loc.located
-
- type 'a and_short_name = 'a * Names.Id.t Loc.located option
-
- type 'a glob_sort_gen =
- | GProp (** representation of [Prop] literal *)
- | GSet (** representation of [Set] literal *)
- | GType of 'a (** representation of [Type] literal *)
-
- type 'a universe_kind =
- | UAnonymous
- | UUnknown
- | UNamed of 'a
-
- type level_info = Libnames.reference universe_kind
- type glob_level = level_info glob_sort_gen
-
- type sort_info = (Libnames.reference * int) option list
- type glob_sort = sort_info glob_sort_gen
-
- type ('a, 'b) gen_universe_decl = {
- univdecl_instance : 'a; (* Declared universes *)
- univdecl_extensible_instance : bool; (* Can new universes be added *)
- univdecl_constraints : 'b; (* Declared constraints *)
- univdecl_extensible_constraints : bool (* Can new constraints be added *) }
-
- type glob_constraint = glob_level * Univ.constraint_type * glob_level
-
- type case_style = Constr.case_style =
- | LetStyle
- | IfStyle
- | LetPatternStyle
- | MatchStyle
- | RegularStyle (** infer printing form from number of constructor *)
- [@@ocaml.deprecated "Alias for Constr.case_style."]
-
- type 'a cast_type =
- | CastConv of 'a
- | CastVM of 'a
- | CastCoerce
- | CastNative of 'a
-
- type 'constr intro_pattern_expr =
- | IntroForthcoming of bool
- | IntroNaming of intro_pattern_naming_expr
- | IntroAction of 'constr intro_pattern_action_expr
- and intro_pattern_naming_expr =
- | IntroIdentifier of Names.Id.t
- | IntroFresh of Names.Id.t
- | IntroAnonymous
- and 'constr intro_pattern_action_expr =
- | IntroWildcard
- | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
- | IntroInjection of ('constr intro_pattern_expr) Loc.located list
- | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located
- | IntroRewrite of bool
- and 'constr or_and_intro_pattern_expr =
- | IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list
- | IntroAndPattern of ('constr intro_pattern_expr) Loc.located list
-
- type quantified_hypothesis =
- | AnonHyp of int
- | NamedHyp of Names.Id.t
-
- type 'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list
-
- type 'a bindings =
- | ImplicitBindings of 'a list
- | ExplicitBindings of 'a explicit_bindings
- | NoBindings
-
- type 'a with_bindings = 'a * 'a bindings
-
- type 'a core_destruction_arg =
- | ElimOnConstr of 'a
- | ElimOnIdent of Names.Id.t Loc.located
- | ElimOnAnonHyp of int
-
- type inversion_kind =
- | SimpleInversion
- | FullInversion
- | FullInversionClear
-
- type multi =
- | Precisely of int
- | UpTo of int
- | RepeatStar
- | RepeatPlus
- type 'id move_location =
- | MoveAfter of 'id
- | MoveBefore of 'id
- | MoveFirst
- | MoveLast
-
- type 'a destruction_arg = clear_flag * 'a core_destruction_arg
-
-end
-
-module Locus :
-sig
- type 'a occurrences_gen =
- | AllOccurrences
- | AllOccurrencesBut of 'a list (** non-empty *)
- | NoOccurrences
- | OnlyOccurrences of 'a list (** non-empty *)
- type occurrences = int occurrences_gen
- type occurrences_expr = (int Misctypes.or_var) occurrences_gen
- type 'a with_occurrences = occurrences_expr * 'a
- type hyp_location_flag =
- InHyp | InHypTypeOnly | InHypValueOnly
- type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
- type 'id clause_expr =
- { onhyps : 'id hyp_location_expr list option;
- concl_occs : occurrences_expr }
- type clause = Names.Id.t clause_expr
- type hyp_location = Names.Id.t * hyp_location_flag
- type goal_location = hyp_location option
-end
-
-(************************************************************************)
-(* End Modules from intf/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from library/ *)
-(************************************************************************)
-
-module Univops :
-sig
- val universes_of_constr : Environ.env -> Constr.constr -> Univ.LSet.t
- val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t
-end
-
-module Nameops :
-sig
-
- open Names
-
- val atompart_of_id : Names.Id.t -> string
-
- val pr_id : Names.Id.t -> Pp.t
- [@@ocaml.deprecated "alias of API.Names.Id.print"]
-
- val pr_name : Names.Name.t -> Pp.t
- [@@ocaml.deprecated "alias of API.Names.Name.print"]
-
- module Name : sig
- include module type of struct include Name end
-
- val map : (Id.t -> Id.t) -> Name.t -> t
- val get_id : t -> Names.Id.t
- val fold_right : (Names.Id.t -> 'a -> 'a) -> t -> 'a -> 'a
-
- end
-
- val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
- [@@ocaml.deprecated "alias of API.Names"]
-
- val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
- [@@ocaml.deprecated "alias of API.Names"]
-
- val add_suffix : Id.t -> string -> Id.t
- val increment_subscript : Id.t -> Id.t
- val make_ident : string -> int option -> Id.t
- val out_name : Name.t -> Id.t
- [@@ocaml.deprecated "alias of API.Names"]
- val pr_lab : Label.t -> Pp.t
- [@@ocaml.deprecated "alias of API.Names"]
-end
-
-module Globnames :
-sig
-
- open Util
-
- type global_reference =
- | VarRef of Names.Id.t
- | ConstRef of Names.Constant.t
- | IndRef of Names.inductive
- | ConstructRef of Names.constructor
-
- type extended_global_reference =
- | TrueGlobal of global_reference
- | SynDef of Names.KerName.t
-
- (* Long term: change implementation so that only 1 kind of order is needed.
- * Today: _env ones are fine grained, which one to pick depends. Eg.
- * - conversion rule are implemented by the non_env ones
- * - pretty printing (of user provided names/aliases) are implemented by
- * the _env ones
- *)
- module Refset : CSig.SetS with type elt = global_reference
- module Refmap : Map.ExtS
- with type key = global_reference and module Set := Refset
-
- module Refset_env : CSig.SetS with type elt = global_reference
- module Refmap_env : Map.ExtS
- with type key = global_reference and module Set := Refset_env
-
- module RefOrdered :
- sig
- type t = global_reference
- val compare : t -> t -> int
- end
-
- val pop_global_reference : global_reference -> global_reference
- val eq_gr : global_reference -> global_reference -> bool
- val destIndRef : global_reference -> Names.inductive
-
- val encode_mind : Names.DirPath.t -> Names.Id.t -> Names.MutInd.t
- val encode_con : Names.DirPath.t -> Names.Id.t -> Names.Constant.t
-
- val global_of_constr : Constr.t -> global_reference
-
- val subst_global : Mod_subst.substitution -> global_reference -> global_reference * Constr.t
- val destConstructRef : global_reference -> Names.constructor
-
- val reference_of_constr : Constr.t -> global_reference
- [@@ocaml.deprecated "alias of API.Globnames.global_of_constr"]
-
- val is_global : global_reference -> Constr.t -> bool
-end
-
-(******************************************************************************)
-(* XXX: Moved from intf *)
-(******************************************************************************)
-module Pattern :
-sig
-
- type case_info_pattern =
- { cip_style : Constr.case_style;
- cip_ind : Names.inductive option;
- cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *)
- cip_extensible : bool (** does this match end with _ => _ ? *) }
-
- type constr_pattern =
- | PRef of Globnames.global_reference
- | PVar of Names.Id.t
- | PEvar of Evar.t * constr_pattern array
- | PRel of int
- | PApp of constr_pattern * constr_pattern array
- | PSoApp of Names.Id.t * constr_pattern list
- | PProj of Names.Projection.t * constr_pattern
- | PLambda of Names.Name.t * constr_pattern * constr_pattern
- | PProd of Names.Name.t * constr_pattern * constr_pattern
- | PLetIn of Names.Name.t * constr_pattern * constr_pattern option * constr_pattern
- | PSort of Misctypes.glob_sort
- | PMeta of Names.Id.t option
- | PIf of constr_pattern * constr_pattern * constr_pattern
- | PCase of case_info_pattern * constr_pattern * constr_pattern *
- (int * bool list * constr_pattern) list (** index of constructor, nb of args *)
- | PFix of Constr.fixpoint
- | PCoFix of Constr.cofixpoint
-
-end
-
-module Evar_kinds :
-sig
- type obligation_definition_status =
- | Define of bool
- | Expand
-
- type matching_var_kind =
- | FirstOrderPatVar of Names.Id.t
- | SecondOrderPatVar of Names.Id.t
-
- type t =
- | ImplicitArg of Globnames.global_reference * (int * Names.Id.t option)
- * bool (** Force inference *)
- | BinderType of Names.Name.t
- | NamedHole of Names.Id.t (* coming from some ?[id] syntax *)
- | QuestionMark of obligation_definition_status * Names.Name.t
- | CasesType of bool (* true = a subterm of the type *)
- | InternalHole
- | TomatchTypeParameter of Names.inductive * int
- | GoalEvar
- | ImpossibleCase
- | MatchingVar of matching_var_kind
- | VarInstance of Names.Id.t
- | SubEvar of Evar.t
-end
-
-module Decl_kinds :
-sig
- type polymorphic = bool
- type cumulative_inductive_flag = bool
-
- type recursivity_kind = Declarations.recursivity_kind =
- | Finite (** = inductive *)
- [@ocaml.deprecated "Please use [Declarations.Finite"]
- | CoFinite (** = coinductive *)
- [@ocaml.deprecated "Please use [Declarations.CoFinite"]
- | BiFinite (** = non-recursive, like in "Record" definitions *)
- [@ocaml.deprecated "Please use [Declarations.BiFinite"]
- [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]
-
- type discharge =
- | DoDischarge
- | NoDischarge
-
- type locality =
- | Discharge
- | Local
- | Global
-
- type definition_object_kind =
- | Definition
- | Coercion
- | SubClass
- | CanonicalStructure
- | Example
- | Fixpoint
- | CoFixpoint
- | Scheme
- | StructureComponent
- | IdentityCoercion
- | Instance
- | Method
- | Let
- type theorem_kind =
- | Theorem
- | Lemma
- | Fact
- | Remark
- | Property
- | Proposition
- | Corollary
- type goal_object_kind =
- | DefinitionBody of definition_object_kind
- | Proof of theorem_kind
- type goal_kind = locality * polymorphic * goal_object_kind
- type assumption_object_kind =
- | Definitional
- | Logical
- | Conjectural
- type logical_kind =
- | IsAssumption of assumption_object_kind
- | IsDefinition of definition_object_kind
- | IsProof of theorem_kind
- type binding_kind =
- | Explicit
- | Implicit
- type private_flag = bool
- type definition_kind = locality * polymorphic * definition_object_kind
-end
-
-module Glob_term :
-sig
- type 'a cases_pattern_r =
- | PatVar of Names.Name.t
- | PatCstr of Names.constructor * 'a cases_pattern_g list * Names.Name.t
- and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
- type cases_pattern = [ `any ] cases_pattern_g
- type existential_name = Names.Id.t
- type 'a glob_constr_r =
- | GRef of Globnames.global_reference * Misctypes.glob_level list option
- (** An identifier that represents a reference to an object defined
- either in the (global) environment or in the (local) context. *)
- | GVar of Names.Id.t
- (** An identifier that cannot be regarded as "GRef".
- Bound variables are typically represented this way. *)
- | GEvar of existential_name * (Names.Id.t * 'a glob_constr_g) list
- | GPatVar of Evar_kinds.matching_var_kind
- | GApp of 'a glob_constr_g * 'a glob_constr_g list
- | GLambda of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g
- | GProd of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g
- | GLetIn of Names.Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g
- | GCases of Constr.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g
- | GLetTuple of Names.Name.t list * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
- | GIf of 'a glob_constr_g * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
- | GRec of 'a fix_kind_g * Names.Id.t array * 'a glob_decl_g list array *
- 'a glob_constr_g array * 'a glob_constr_g array
- | GSort of Misctypes.glob_sort
- | GHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
- | GCast of 'a glob_constr_g * 'a glob_constr_g Misctypes.cast_type
-
- and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
-
- and 'a glob_decl_g = Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g option * 'a glob_constr_g
-
- and 'a fix_recursion_order_g =
- | GStructRec
- | GWfRec of 'a glob_constr_g
- | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option
-
- and 'a fix_kind_g =
- | GFix of ((int option * 'a fix_recursion_order_g) array * int)
- | GCoFix of int
-
- and 'a predicate_pattern_g =
- Names.Name.t * (Names.inductive * Names.Name.t list) Loc.located option
-
- and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g)
-
- and 'a tomatch_tuples_g = 'a tomatch_tuple_g list
-
- and 'a cases_clause_g = (Names.Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) Loc.located
- and 'a cases_clauses_g = 'a cases_clause_g list
-
- type glob_constr = [ `any ] glob_constr_g
- type tomatch_tuple = [ `any ] tomatch_tuple_g
- type tomatch_tuples = [ `any ] tomatch_tuples_g
- type cases_clause = [ `any ] cases_clause_g
- type cases_clauses = [ `any ] cases_clauses_g
- type glob_decl = [ `any ] glob_decl_g
- type fix_kind = [ `any ] fix_kind_g
- type predicate_pattern = [ `any ] predicate_pattern_g
- type any_glob_constr =
- | AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
-
-end
-
-module Notation_term :
-sig
- type scope_name = string
- type notation_var_instance_type =
- | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList
- type tmp_scope_name = scope_name
-
- type subscopes = tmp_scope_name option * scope_name list
- type notation_constr =
- | NRef of Globnames.global_reference
- | NVar of Names.Id.t
- | NApp of notation_constr * notation_constr list
- | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
- | NList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool
- | NLambda of Names.Name.t * notation_constr * notation_constr
- | NProd of Names.Name.t * notation_constr * notation_constr
- | NBinderList of Names.Id.t * Names.Id.t * notation_constr * notation_constr
- | NLetIn of Names.Name.t * notation_constr * notation_constr option * notation_constr
- | NCases of Constr.case_style * notation_constr option *
- (notation_constr * (Names.Name.t * (Names.inductive * Names.Name.t list) option)) list *
- (Glob_term.cases_pattern list * notation_constr) list
- | NLetTuple of Names.Name.t list * (Names.Name.t * notation_constr option) *
- notation_constr * notation_constr
- | NIf of notation_constr * (Names.Name.t * notation_constr option) *
- notation_constr * notation_constr
- | NRec of Glob_term.fix_kind * Names.Id.t array *
- (Names.Name.t * notation_constr option * notation_constr) list array *
- notation_constr array * notation_constr array
- | NSort of Misctypes.glob_sort
- | NCast of notation_constr * notation_constr Misctypes.cast_type
- type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list *
- notation_constr
- type precedence = int
- type parenRelation =
- | L | E | Any | Prec of precedence
- type tolerability = precedence * parenRelation
-end
-
-module Constrexpr :
-sig
-
- type binder_kind =
- | Default of Decl_kinds.binding_kind
- | Generalized of Decl_kinds.binding_kind * Decl_kinds.binding_kind * bool
-
- type explicitation =
- | ExplByPos of int * Names.Id.t option
- | ExplByName of Names.Id.t
- type sign = bool
- type raw_natural_number = string
- type prim_token =
- | Numeral of raw_natural_number * sign
- | String of string
-
- type notation = string
- type instance_expr = Misctypes.glob_level list
- type proj_flag = int option
- type abstraction_kind =
- | AbsLambda
- | AbsPi
-
- type cases_pattern_expr_r =
- | CPatAlias of cases_pattern_expr * Names.Id.t
- | CPatCstr of Libnames.reference
- * cases_pattern_expr list option * cases_pattern_expr list
- (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
- | CPatAtom of Libnames.reference option
- | CPatOr of cases_pattern_expr list
- | CPatNotation of notation * cases_pattern_notation_substitution
- * cases_pattern_expr list
- | CPatPrim of prim_token
- | CPatRecord of (Libnames.reference * cases_pattern_expr) list
- | CPatDelimiters of string * cases_pattern_expr
- | CPatCast of cases_pattern_expr * constr_expr
- and cases_pattern_expr = cases_pattern_expr_r CAst.t
-
- and cases_pattern_notation_substitution =
- cases_pattern_expr list * cases_pattern_expr list list
-
- and constr_expr_r =
- | CRef of Libnames.reference * instance_expr option
- | CFix of Names.Id.t Loc.located * fix_expr list
- | CCoFix of Names.Id.t Loc.located * cofix_expr list
- | CProdN of binder_expr list * constr_expr
- | CLambdaN of binder_expr list * constr_expr
- | CLetIn of Names.Name.t Loc.located * constr_expr * constr_expr option * constr_expr
- | CAppExpl of (proj_flag * Libnames.reference * instance_expr option) * constr_expr list
- | CApp of (proj_flag * constr_expr) *
- (constr_expr * explicitation Loc.located option) list
- | CRecord of (Libnames.reference * constr_expr) list
- | CCases of Constr.case_style
- * constr_expr option
- * case_expr list
- * branch_expr list
- | CLetTuple of Names.Name.t Loc.located list * (Names.Name.t Loc.located option * constr_expr option) *
- constr_expr * constr_expr
- | CIf of constr_expr * (Names.Name.t Loc.located option * constr_expr option)
- * constr_expr * constr_expr
- | CHole of Evar_kinds.t option * Misctypes.intro_pattern_naming_expr * Genarg.raw_generic_argument option
- | CPatVar of Names.Id.t
- | CEvar of Names.Id.t * (Names.Id.t * constr_expr) list
- | CSort of Misctypes.glob_sort
- | CCast of constr_expr * constr_expr Misctypes.cast_type
- | CNotation of notation * constr_notation_substitution
- | CGeneralization of Decl_kinds.binding_kind * abstraction_kind option * constr_expr
- | CPrim of prim_token
- | CDelimiters of string * constr_expr
- and constr_expr = constr_expr_r CAst.t
-
- and case_expr = constr_expr * Names.Name.t Loc.located option * cases_pattern_expr option
-
- and branch_expr =
- (cases_pattern_expr list list * constr_expr) Loc.located
-
- and binder_expr =
- Names.Name.t Loc.located list * binder_kind * constr_expr
-
- and fix_expr =
- Names.Id.t Loc.located * (Names.Id.t Loc.located option * recursion_order_expr) *
- local_binder_expr list * constr_expr * constr_expr
-
- and cofix_expr =
- Names.Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr
-
- and recursion_order_expr =
- | CStructRec
- | CWfRec of constr_expr
- | CMeasureRec of constr_expr * constr_expr option
-
- and local_binder_expr =
- | CLocalAssum of Names.Name.t Loc.located list * binder_kind * constr_expr
- | CLocalDef of Names.Name.t Loc.located * constr_expr * constr_expr option
- | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located
-
- and constr_notation_substitution =
- constr_expr list *
- constr_expr list list *
- local_binder_expr list list
-
- type constr_pattern_expr = constr_expr
-end
-
-module Genredexpr :
-sig
-
- (** The parsing produces initially a list of [red_atom] *)
- type 'a red_atom =
- | FBeta
- | FMatch
- | FFix
- | FCofix
- | FZeta
- | FConst of 'a list
- | FDeltaBut of 'a list
-
- (** This list of atoms is immediately converted to a [glob_red_flag] *)
- type 'a glob_red_flag = {
- rBeta : bool;
- rMatch : bool;
- rFix : bool;
- rCofix : bool;
- rZeta : bool;
- rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
- rConst : 'a list
- }
-
- (** Generic kinds of reductions *)
- type ('a,'b,'c) red_expr_gen =
- | Red of bool
- | Hnf
- | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
- | Cbv of 'b glob_red_flag
- | Cbn of 'b glob_red_flag
- | Lazy of 'b glob_red_flag
- | Unfold of 'b Locus.with_occurrences list
- | Fold of 'a list
- | Pattern of 'a Locus.with_occurrences list
- | ExtraRedExpr of string
- | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
- | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
-
- type ('a,'b,'c) may_eval =
- | ConstrTerm of 'a
- | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
- | ConstrContext of Names.Id.t Loc.located * 'a
- | ConstrTypeOf of 'a
-
- type r_trm = Constrexpr.constr_expr
- type r_pat = Constrexpr.constr_pattern_expr
- type r_cst = Libnames.reference Misctypes.or_by_notation
- type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
-end
-
-(******************************************************************************)
-(* XXX: end of moved from intf *)
-(******************************************************************************)
-
-module Libobject :
-sig
- type obj
- type 'a substitutivity =
- | Dispose
- | Substitute of 'a
- | Keep of 'a
- | Anticipate of 'a
-
- type 'a object_declaration = {
- object_name : string;
- cache_function : Libnames.object_name * 'a -> unit;
- load_function : int -> Libnames.object_name * 'a -> unit;
- open_function : int -> Libnames.object_name * 'a -> unit;
- classify_function : 'a -> 'a substitutivity;
- subst_function : Mod_subst.substitution * 'a -> 'a;
- discharge_function : Libnames.object_name * 'a -> 'a option;
- rebuild_function : 'a -> 'a
- }
- val declare_object : 'a object_declaration -> ('a -> obj)
- val default_object : string -> 'a object_declaration
- val object_tag : obj -> string
-end
-
-module Summary :
-sig
-
- type frozen
-
- type marshallable =
- [ `Yes (* Full data will be marshalled to disk *)
- | `No (* Full data will be store in memory, e.g. for Undo *)
- | `Shallow ] (* Only part of the data will be marshalled to a slave process *)
-
- type 'a summary_declaration =
- { freeze_function : marshallable -> 'a;
- unfreeze_function : 'a -> unit;
- init_function : unit -> unit; }
-
- val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
- val declare_summary : string -> 'a summary_declaration -> unit
- module Local :
- sig
- type 'a local_ref
- val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref
- val (:=) : 'a local_ref -> 'a -> unit
- val (!) : 'a local_ref -> 'a
- end
-end
-
-module Nametab :
-sig
- exception GlobalizationError of Libnames.qualid
-
- val global : Libnames.reference -> Globnames.global_reference
- val global_of_path : Libnames.full_path -> Globnames.global_reference
- val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid
- val path_of_global : Globnames.global_reference -> Libnames.full_path
- val locate_extended : Libnames.qualid -> Globnames.extended_global_reference
- val full_name_module : Libnames.qualid -> Names.DirPath.t
- val pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.t
- val basename_of_global : Globnames.global_reference -> Names.Id.t
-
- type visibility =
- | Until of int
- | Exactly of int
-
- val error_global_not_found : ?loc:Loc.t -> Libnames.qualid -> 'a
- val shortest_qualid_of_module : Names.ModPath.t -> Libnames.qualid
- val dirpath_of_module : Names.ModPath.t -> Names.DirPath.t
- val locate_module : Libnames.qualid -> Names.ModPath.t
- val dirpath_of_global : Globnames.global_reference -> Names.DirPath.t
- val locate : Libnames.qualid -> Globnames.global_reference
- val locate_constant : Libnames.qualid -> Names.Constant.t
-
- (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)
-
- module type UserName = sig
- type t
- val equal : t -> t -> bool
- val to_string : t -> string
- val repr : t -> Names.Id.t * Names.Id.t list
- end
-
- module type EqualityType =
- sig
- type t
- val equal : t -> t -> bool
- end
-
- module type NAMETREE = sig
- type elt
- type t
- type user_name
-
- val empty : t
- val push : visibility -> user_name -> elt -> t -> t
- val locate : Libnames.qualid -> t -> elt
- val find : user_name -> t -> elt
- val exists : user_name -> t -> bool
- val user_name : Libnames.qualid -> t -> user_name
- val shortest_qualid : Names.Id.Set.t -> user_name -> t -> Libnames.qualid
- val find_prefixes : Libnames.qualid -> t -> elt list
- end
-
- module Make (U : UserName) (E : EqualityType) :
- NAMETREE with type user_name = U.t and type elt = E.t
-
-end
-
-module Global :
-sig
- val env : unit -> Environ.env
- val lookup_mind : Names.MutInd.t -> Declarations.mutual_inductive_body
- val lookup_constant : Names.Constant.t -> Declarations.constant_body
- val lookup_module : Names.ModPath.t -> Declarations.module_body
- val lookup_modtype : Names.ModPath.t -> Declarations.module_type_body
- val lookup_inductive : Names.inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body
- val constant_of_delta_kn : Names.KerName.t -> Names.Constant.t
- val register :
- Retroknowledge.field -> Constr.t -> Constr.t -> unit
- val env_of_context : Environ.named_context_val -> Environ.env
- val is_polymorphic : Globnames.global_reference -> bool
-
- val constr_of_global_in_context : Environ.env ->
- Globnames.global_reference -> Constr.types * Univ.AUContext.t
-
- val type_of_global_in_context : Environ.env ->
- Globnames.global_reference -> Constr.types * Univ.AUContext.t
-
- val current_dirpath : unit -> Names.DirPath.t
- val body_of_constant_body : Declarations.constant_body -> (Constr.t * Univ.AUContext.t) option
- val body_of_constant : Names.Constant.t -> (Constr.t * Univ.AUContext.t) option
- val add_constraints : Univ.Constraint.t -> unit
-end
-
-module Lib : sig
- type is_type = bool
- type export = bool option
- type node =
- | Leaf of Libobject.obj (* FIX: horrible hack (wrt. Enrico) *)
- | CompilingLibrary of Libnames.object_prefix
- | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen
- | ClosedModule of library_segment
- | OpenedSection of Libnames.object_prefix * Summary.frozen
- | ClosedSection of library_segment
-
- and library_segment = (Libnames.object_name * node) list
-
- val current_mp : unit -> Names.ModPath.t
- val is_modtype : unit -> bool
- val is_module : unit -> bool
- val sections_are_opened : unit -> bool
- val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
- val contents : unit -> library_segment
- val cwd : unit -> Names.DirPath.t
- val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
- val make_kn : Names.Id.t -> Names.KerName.t
- val make_path : Names.Id.t -> Libnames.full_path
- val discharge_con : Names.Constant.t -> Names.Constant.t
- val discharge_inductive : Names.inductive -> Names.inductive
-end
-
-module Declaremods :
-sig
-
- val append_end_library_hook : (unit -> unit) -> unit
-
-end
-
-module Library :
-sig
- val library_is_loaded : Names.DirPath.t -> bool
- val loaded_libraries : unit -> Names.DirPath.t list
-end
-
-module States :
-sig
- type state
-
- val with_state_protection : ('a -> 'b) -> 'a -> 'b
-end
-
-module Kindops :
-sig
- val logical_kind_of_goal_kind : Decl_kinds.goal_object_kind -> Decl_kinds.logical_kind
-end
-
-module Goptions :
-sig
- type option_name = string list
- type 'a option_sig =
- {
- optdepr : bool;
- optname : string;
- optkey : option_name;
- optread : unit -> 'a;
- optwrite : 'a -> unit
- }
-
- type 'a write_function = 'a -> unit
-
- val declare_bool_option : ?preprocess:(bool -> bool) ->
- bool option_sig -> bool write_function
- val declare_int_option : ?preprocess:(int option -> int option) ->
- int option option_sig -> int option write_function
- val declare_string_option: ?preprocess:(string -> string) ->
- string option_sig -> string write_function
- val set_bool_option_value : option_name -> bool -> unit
-end
-
-module Keys :
-sig
- type key
- val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
- val declare_equiv_keys : key -> key -> unit
- val pr_keys : (Globnames.global_reference -> Pp.t) -> Pp.t
-end
-
-module Coqlib :
-sig
-
- type coq_eq_data = { eq : Globnames.global_reference;
- ind : Globnames.global_reference;
- refl : Globnames.global_reference;
- sym : Globnames.global_reference;
- trans: Globnames.global_reference;
- congr: Globnames.global_reference;
- }
-
- type coq_sigma_data = {
- proj1 : Globnames.global_reference;
- proj2 : Globnames.global_reference;
- elim : Globnames.global_reference;
- intro : Globnames.global_reference;
- typ : Globnames.global_reference }
- val find_reference : string -> string list -> string -> Globnames.global_reference
- val check_required_library : string list -> unit
- val logic_module_name : string list
- val glob_true : Globnames.global_reference
- val glob_false : Globnames.global_reference
- val glob_O : Globnames.global_reference
- val glob_S : Globnames.global_reference
- val nat_path : Libnames.full_path
- val datatypes_module_name : string list
- val glob_eq : Globnames.global_reference
- val build_coq_eq_sym : Globnames.global_reference Util.delayed
- val build_coq_False : Globnames.global_reference Util.delayed
- val build_coq_not : Globnames.global_reference Util.delayed
- val build_coq_eq : Globnames.global_reference Util.delayed
- val build_coq_eq_data : coq_eq_data Util.delayed
- val path_of_O : Names.constructor
- val path_of_S : Names.constructor
- val build_prod : coq_sigma_data Util.delayed
- val build_coq_True : Globnames.global_reference Util.delayed
- val coq_iff_ref : Globnames.global_reference lazy_t
- val build_coq_iff_left_proj : Globnames.global_reference Util.delayed
- val build_coq_iff_right_proj : Globnames.global_reference Util.delayed
- val init_modules : string list list
- val build_coq_eq_refl : Globnames.global_reference Util.delayed
- val arith_modules : string list list
- val zarith_base_modules : string list list
- val gen_reference_in_modules : string -> string list list-> string -> Globnames.global_reference
- val jmeq_module_name : string list
- val coq_eq_ref : Globnames.global_reference lazy_t
- val coq_not_ref : Globnames.global_reference lazy_t
- val coq_or_ref : Globnames.global_reference lazy_t
- val build_coq_and : Globnames.global_reference Util.delayed
- val build_coq_or : Globnames.global_reference Util.delayed
- val build_coq_I : Globnames.global_reference Util.delayed
- val coq_reference : string -> string list -> string -> Globnames.global_reference
-end
-
-(************************************************************************)
-(* End of modules from library/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from engine/ *)
-(************************************************************************)
-
-module Universes :
-sig
- type universe_binders
- type universe_opt_subst
- val fresh_inductive_instance : Environ.env -> Names.inductive -> Constr.pinductive Univ.in_universe_context_set
- val new_Type : unit -> Constr.types
- val type_of_global : Globnames.global_reference -> Constr.types Univ.in_universe_context_set
- val constr_of_global : Globnames.global_reference -> Constr.t
- val new_univ_level : unit -> Univ.Level.t
- val new_sort_in_family : Sorts.family -> Sorts.t
- val pr_with_global_universes : Univ.Level.t -> Pp.t
- val pr_universe_opt_subst : universe_opt_subst -> Pp.t
- type universe_constraint
-
- module Constraints :
- sig
- type t
- val pr : t -> Pp.t
- end
-
- type universe_constraints = Constraints.t
- [@@ocaml.deprecated "Use Constraints.t"]
-
-end
-
-module UState :
-sig
- type t
- val context : t -> Univ.UContext.t
- val context_set : t -> Univ.ContextSet.t
- val of_context_set : Univ.ContextSet.t -> t
-
- val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
- val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
-
- type rigid =
- | UnivRigid
- | UnivFlexible of bool
-
-end
-
-module Evd :
-sig
-
- type evar = Evar.t
- [@@ocaml.deprecated "use Evar.t"]
-
- val string_of_existential : Evar.t -> string
- [@@ocaml.deprecated "use Evar.print"]
-
- type evar_constraint = Reduction.conv_pb * Environ.env * Constr.t * Constr.t
-
- (* --------------------------------- *)
-
- (* evar info *)
-
- module Store :
- sig
- type t
- val empty : t
- end
-
- module Filter :
- sig
- type t
- val repr : t -> bool list option
- end
-
- (** This value defines the refinement of a given {i evar} *)
- type evar_body =
- | Evar_empty (** given {i evar} was not yet refined *)
- | Evar_defined of Constr.t (** given {i var} was refined to the indicated term *)
-
- (** all the information we have concerning some {i evar} *)
- type evar_info =
- {
- evar_concl : Constr.t;
- evar_hyps : Environ.named_context_val;
- evar_body : evar_body;
- evar_filter : Filter.t;
- evar_source : Evar_kinds.t Loc.located;
- evar_candidates : Constr.t list option; (* if not None, list of allowed instances *)
- evar_extra : Store.t
- }
-
- val evar_concl : evar_info -> Constr.t
- val evar_body : evar_info -> evar_body
- val evar_context : evar_info -> Context.Named.t
- val instantiate_evar_array : evar_info -> Constr.t -> Constr.t array -> Constr.t
- val evar_filtered_env : evar_info -> Environ.env
- val evar_hyps : evar_info -> Environ.named_context_val
-
- (* ------------------------------------ *)
-
- (* evar map *)
-
- type evar_map
- type open_constr = evar_map * Constr.t
-
- open Util
-
- module Metaset : Set.S with type elt = Constr.metavariable
-
- type rigid = UState.rigid =
- | UnivRigid
- | UnivFlexible of bool
-
- type 'a freelisted = {
- rebus : 'a;
- freemetas : Metaset.t
- }
-
- type instance_constraint = IsSuperType | IsSubType | Conv
-
- type instance_typing_status =
- CoerceToType | TypeNotProcessed | TypeProcessed
-
- type instance_status = instance_constraint * instance_typing_status
-
- type clbinding =
- | Cltyp of Names.Name.t * Constr.t freelisted
- | Clval of Names.Name.t * (Constr.t freelisted * instance_status) * Constr.t freelisted
-
- val empty : evar_map
- val from_env : Environ.env -> evar_map
- val find : evar_map -> Evar.t -> evar_info
- val find_undefined : evar_map -> Evar.t -> evar_info
- val is_defined : evar_map -> Evar.t -> bool
- val mem : evar_map -> Evar.t -> bool
- val add : evar_map -> Evar.t -> evar_info -> evar_map
- val evar_universe_context : evar_map -> UState.t
- val set_universe_context : evar_map -> UState.t -> evar_map
- val universes : evar_map -> UGraph.t
- val define : Evar.t -> Constr.t -> evar_map -> evar_map
- val fold : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
- val evar_key : Names.Id.t -> evar_map -> Evar.t
-
- val create_evar_defs : evar_map -> evar_map
-
- val meta_declare : Constr.metavariable -> Constr.types -> ?name:Names.Name.t -> evar_map -> evar_map
-
- val clear_metas : evar_map -> evar_map
-
- (** Allocates a new evar that represents a {i sort}. *)
- val new_sort_variable : ?loc:Loc.t -> ?name:Names.Id.t -> rigid -> evar_map -> evar_map * Sorts.t
-
- val remove : evar_map -> Evar.t -> evar_map
- val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> Environ.env ->
- evar_map -> Globnames.global_reference -> evar_map * Constr.t
- val evar_filtered_context : evar_info -> Context.Named.t
- val fresh_inductive_instance : ?loc:Loc.t -> Environ.env -> evar_map -> Names.inductive -> evar_map * Constr.pinductive
- val fold_undefined : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
-
- val universe_context_set : evar_map -> Univ.ContextSet.t
- val evar_ident : Evar.t -> evar_map -> Names.Id.t option
- val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
- val universe_binders : evar_map -> Universes.universe_binders
- val nf_constraints : evar_map -> evar_map
- val from_ctx : UState.t -> evar_map
-
- val to_universe_context : evar_map -> Univ.UContext.t
- val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry
- val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes
-
- val meta_list : evar_map -> (Constr.metavariable * clbinding) list
-
- val meta_defined : evar_map -> Constr.metavariable -> bool
-
- val meta_name : evar_map -> Constr.metavariable -> Names.Name.t
-
- module MonadR :
- sig
- module List :
- sig
- val map_right : ('a -> evar_map -> evar_map * 'b) -> 'a list -> evar_map -> evar_map * 'b list
- end
- end
-
- type 'a sigma = {
- it : 'a ;
- sigma : evar_map
- }
-
- val sig_sig : 'a sigma -> evar_map
-
- val sig_it : 'a sigma -> 'a
-
- type 'a in_evar_universe_context = 'a * UState.t
-
- val univ_flexible : rigid
- val univ_flexible_alg : rigid
- val empty_evar_universe_context : UState.t
- val union_evar_universe_context : UState.t -> UState.t -> UState.t
- val merge_universe_context : evar_map -> UState.t -> evar_map
-
- type unsolvability_explanation =
- | SeveralInstancesFound of int
-
- (** Return {i ids} of all {i evars} that occur in a given term. *)
- val evars_of_term : Constr.t -> Evar.Set.t
-
- val evar_universe_context_of : Univ.ContextSet.t -> UState.t
- [@@ocaml.deprecated "alias of API.UState.of_context_set"]
-
- val evar_context_universe_context : UState.t -> Univ.UContext.t
- [@@ocaml.deprecated "alias of API.UState.context"]
-
- type evar_universe_context = UState.t
- [@@ocaml.deprecated "alias of API.UState.t"]
-
- val existential_opt_value : evar_map -> Constr.existential -> Constr.t option
- val existential_value : evar_map -> Constr.existential -> Constr.t
-
- exception NotInstantiatedEvar
-
- val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> Environ.env -> evar_map -> Sorts.family -> evar_map * Sorts.t
-end
-
-module EConstr :
-sig
- type t
- type constr = t
- type types = t
- type unsafe_judgment = (constr, types) Environ.punsafe_judgment
- type named_declaration = (constr, types) Context.Named.Declaration.pt
- type named_context = (constr, types) Context.Named.pt
- type rel_context = (constr, types) Context.Rel.pt
- type rel_declaration = (constr, types) Context.Rel.Declaration.pt
- type existential = constr Constr.pexistential
- module ESorts :
- sig
- type t
- (** Type of sorts up-to universe unification. Essentially a wrapper around
- Sorts.t so that normalization is ensured statically. *)
-
- val make : Sorts.t -> t
- (** Turn a sort into an up-to sort. *)
-
- val kind : Evd.evar_map -> t -> Sorts.t
- (** Returns the view into the current sort. Note that the kind of a variable
- may change if the unification state of the evar map changes. *)
-
- end
-
- module EInstance :
- sig
- type t
- (** Type of universe instances up-to universe unification. Similar to
- {ESorts.t} for {Univ.Instance.t}. *)
-
- val make : Univ.Instance.t -> t
- val kind : Evd.evar_map -> t -> Univ.Instance.t
- val empty : t
- val is_empty : t -> bool
- end
-
- val of_constr : Constr.t -> constr
-
- val kind : Evd.evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) Constr.kind_of_term
-
- val mkArrow : constr -> constr -> constr
- val mkInd : Names.inductive -> t
- val mkProp : constr
- val mkProd : Names.Name.t * constr * constr -> constr
- val mkRel : int -> constr
- val mkSort : Sorts.t -> constr
- val mkVar : Names.Id.t -> constr
- val mkLambda : Names.Name.t * constr * constr -> constr
- val mkLambda_or_LetIn : rel_declaration -> constr -> constr
- val mkApp : constr * constr array -> constr
- val mkEvar : constr Constr.pexistential -> constr
-
- val mkMeta : Constr.metavariable -> constr
-
- val mkConstructU : Names.constructor * EInstance.t -> constr
- val mkLetIn : Names.Name.t * constr * constr * constr -> constr
- val mkProd_or_LetIn : rel_declaration -> constr -> constr
- val mkCast : constr * Constr.cast_kind * constr -> constr
- val mkNamedLambda : Names.Id.t -> types -> constr -> constr
- val mkNamedProd : Names.Id.t -> types -> types -> types
-
- val isCast : Evd.evar_map -> t -> bool
- val isEvar : Evd.evar_map -> constr -> bool
- val isInd : Evd.evar_map -> constr -> bool
- val isRel : Evd.evar_map -> constr -> bool
- val isSort : Evd.evar_map -> constr -> bool
- val isVar : Evd.evar_map -> constr -> bool
- val isConst : Evd.evar_map -> constr -> bool
- val isConstruct : Evd.evar_map -> constr -> bool
-
- val destInd : Evd.evar_map -> constr -> Names.inductive * EInstance.t
- val destVar : Evd.evar_map -> constr -> Names.Id.t
- val destEvar : Evd.evar_map -> constr -> constr Constr.pexistential
- val destRel : Evd.evar_map -> constr -> int
- val destProd : Evd.evar_map -> constr -> Names.Name.t * types * types
- val destLambda : Evd.evar_map -> constr -> Names.Name.t * types * constr
- val destApp : Evd.evar_map -> constr -> constr * constr array
- val destConst : Evd.evar_map -> constr -> Names.Constant.t * EInstance.t
- val destConstruct : Evd.evar_map -> constr -> Names.constructor * EInstance.t
- val destFix : Evd.evar_map -> t -> (t, t) Constr.pfixpoint
- val destCast : Evd.evar_map -> t -> t * Constr.cast_kind * t
-
- val mkConstruct : Names.constructor -> constr
-
- val compose_lam : (Names.Name.t * constr) list -> constr -> constr
-
- val decompose_lam : Evd.evar_map -> constr -> (Names.Name.t * constr) list * constr
- val decompose_lam_n_assum : Evd.evar_map -> int -> constr -> rel_context * constr
- val decompose_app : Evd.evar_map -> constr -> constr * constr list
- val decompose_prod : Evd.evar_map -> constr -> (Names.Name.t * constr) list * constr
- val decompose_prod_assum : Evd.evar_map -> constr -> rel_context * constr
-
- val applist : constr * constr list -> constr
-
- val to_constr : Evd.evar_map -> constr -> Constr.t
-
- val push_rel : rel_declaration -> Environ.env -> Environ.env
-
- module Unsafe :
- sig
- val to_constr : constr -> Constr.t
-
- val to_rel_decl : (constr, types) Context.Rel.Declaration.pt -> (Constr.constr, Constr.types) Context.Rel.Declaration.pt
-
- (** Physical identity. Does not care for defined evars. *)
-
- val to_named_decl : (constr, types) Context.Named.Declaration.pt -> (Constr.constr, Constr.types) Context.Named.Declaration.pt
-
- val to_instance : EInstance.t -> Univ.Instance.t
- end
-
- module Vars :
- sig
- val substnl : t list -> int -> t -> t
- val noccurn : Evd.evar_map -> int -> constr -> bool
- val closed0 : Evd.evar_map -> constr -> bool
- val subst1 : constr -> constr -> constr
- val substl : constr list -> constr -> constr
- val lift : int -> constr -> constr
- val liftn : int -> int -> t -> t
- val subst_var : Names.Id.t -> t -> t
- val subst_vars : Names.Id.t list -> t -> t
- end
-
- val fresh_global :
- ?loc:Loc.t -> ?rigid:UState.rigid -> ?names:Univ.Instance.t -> Environ.env ->
- Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * t
-
- val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (constr, types) Context.Named.Declaration.pt
- val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (constr, types) Context.Rel.Declaration.pt
- val kind_of_type : Evd.evar_map -> constr -> (constr, constr) Term.kind_of_type
- val to_lambda : Evd.evar_map -> int -> constr -> constr
- val it_mkLambda_or_LetIn : constr -> rel_context -> constr
- val push_rel_context : rel_context -> Environ.env -> Environ.env
- val eq_constr : Evd.evar_map -> constr -> constr -> bool
- val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
- val fold : Evd.evar_map -> ('a -> constr -> 'a) -> 'a -> constr -> 'a
- val existential_type : Evd.evar_map -> existential -> types
- val iter : Evd.evar_map -> (constr -> unit) -> constr -> unit
- val eq_constr_universes : Evd.evar_map -> constr -> constr -> Universes.Constraints.t option
- val eq_constr_nounivs : Evd.evar_map -> constr -> constr -> bool
- val compare_constr : Evd.evar_map -> (constr -> constr -> bool) -> constr -> constr -> bool
- val isApp : Evd.evar_map -> constr -> bool
- val it_mkProd_or_LetIn : constr -> rel_context -> constr
- val push_named : named_declaration -> Environ.env -> Environ.env
- val destCase : Evd.evar_map -> constr -> Constr.case_info * constr * constr * constr array
- val decompose_lam_assum : Evd.evar_map -> constr -> rel_context * constr
- val mkConst : Names.Constant.t -> constr
- val mkCase : Constr.case_info * constr * constr * constr array -> constr
- val named_context : Environ.env -> named_context
- val val_of_named_context : named_context -> Environ.named_context_val
- val mkFix : (t, t) Constr.pfixpoint -> t
- val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t
- val isMeta : Evd.evar_map -> t -> bool
-
- val destMeta : Evd.evar_map -> t -> Constr.metavariable
-
- val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
- val mkNamedLetIn : Names.Id.t -> constr -> types -> constr -> constr
- val map : Evd.evar_map -> (t -> t) -> t -> t
- val mkConstU : Names.Constant.t * EInstance.t -> t
- val isProd : Evd.evar_map -> t -> bool
- val mkConstructUi : (Names.inductive * EInstance.t) * int -> t
- val isLambda : Evd.evar_map -> t -> bool
-end
-
-module Namegen :
-sig
- (** *)
-
- (** [next_ident_away original_id unwanted_ids] returns a new identifier as close as possible
- to the [original_id] while avoiding all [unwanted_ids].
-
- In particular:
- {ul {- if [original_id] does not appear in the list of [unwanted_ids], then [original_id] is returned.}
- {- if [original_id] appears in the list of [unwanted_ids],
- then this function returns a new id that:
- {ul {- has the same {i root} as the [original_id],}
- {- does not occur in the list of [unwanted_ids],}
- {- has the smallest possible {i subscript}.}}}}
-
- where by {i subscript} of some identifier we mean last part of it that is composed
- only from (decimal) digits and by {i root} of some identifier we mean
- the whole identifier except for the {i subscript}.
-
- E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *)
- val next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
-
- val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string
- val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t
- val next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
- val default_dependent_ident : Names.Id.t
- val next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
- val rename_bound_vars_as_displayed :
- Evd.evar_map -> Names.Id.Set.t -> Names.Name.t list -> EConstr.types -> EConstr.types
-end
-
-module Termops :
-sig
- val it_mkLambda_or_LetIn : Constr.t -> Context.Rel.t -> Constr.t
- val local_occur_var : Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
- val occur_var : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
- val pr_evar_info : Evd.evar_info -> Pp.t
-
- val print_constr : EConstr.constr -> Pp.t
- val pr_sort_family : Sorts.family -> Pp.t
-
- (** [dependent m t] tests whether [m] is a subterm of [t] *)
- val dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
-
- (** [pop c] returns a copy of [c] with decremented De Bruijn indexes *)
- val pop : EConstr.constr -> EConstr.constr
-
- (** Does a given term contain an existential variable? *)
- val occur_existential : Evd.evar_map -> EConstr.constr -> bool
-
- (** [map_constr_with_binders_left_to_right g f acc c] maps [f updated_acc] on all the immediate subterms of [c].
- {ul {- if a given immediate subterm of [c] is not below a binder, then [updated_acc] is the same as [acc].}
- {- if a given immediate subterm of [c] is below a binder [b], then [updated_acc] is computed as [g b acc].}} *)
- val map_constr_with_binders_left_to_right :
- Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr
-
- (** Remove the outer-most {!Constr.kind_of_term.Cast} from a given term. *)
- val strip_outer_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr
-
- (** [nb_lam] ⟦[fun (x1:t1)...(xn:tn) => c]⟧ where [c] is not an abstraction gives [n].
- Casts are ignored. *)
- val nb_lam : Evd.evar_map -> EConstr.constr -> int
-
- (** [push_rel_assum env_assumtion env] adds a given {i env assumption} to the {i env context} of a given {i environment}. *)
- val push_rel_assum : Names.Name.t * EConstr.types -> Environ.env -> Environ.env
-
- (** [push_rels_assum env_assumptions env] adds given {i env assumptions} to the {i env context} of a given {i environment}. *)
- val push_rels_assum : (Names.Name.t * Constr.types) list -> Environ.env -> Environ.env
-
- type meta_value_map = (Constr.metavariable * Constr.t) list
-
- val last_arg : Evd.evar_map -> EConstr.constr -> EConstr.constr
- val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Names.Name.t * 't) list
- val prod_applist : Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr
- val nb_prod : Evd.evar_map -> EConstr.constr -> int
- val is_section_variable : Names.Id.t -> bool
- val ids_of_rel_context : ('c, 't) Context.Rel.pt -> Names.Id.t list
- val subst_term : Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constr
- val global_vars_set_of_decl : Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Names.Id.Set.t
- val vars_of_env: Environ.env -> Names.Id.Set.t
- val ids_of_named_context : ('c, 't) Context.Named.pt -> Names.Id.t list
- val ids_of_context : Environ.env -> Names.Id.t list
- val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference * EConstr.EInstance.t
- val print_named_context : Environ.env -> Pp.t
- val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
- val clear_named_body : Names.Id.t -> Environ.env -> Environ.env
- val is_Prop : Evd.evar_map -> EConstr.constr -> bool
- val is_Set : Evd.evar_map -> EConstr.constr -> bool
- val is_Type : Evd.evar_map -> EConstr.constr -> bool
- val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool
-
- val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
-
- val occur_var_in_decl :
- Environ.env -> Evd.evar_map ->
- Names.Id.t -> EConstr.named_declaration -> bool
-
- val subst_meta : meta_value_map -> Constr.t -> Constr.t
-
- val free_rels : Evd.evar_map -> EConstr.constr -> Int.Set.t
-
- val occur_term : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
- [@@ocaml.deprecated "alias of API.Termops.dependent"]
-
- val replace_term : Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
- val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
- val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
- val pr_metaset : Evd.Metaset.t -> Pp.t
- val pr_evar_map : ?with_univs:bool -> int option -> Evd.evar_map -> Pp.t
- val pr_evar_universe_context : UState.t -> Pp.t
-end
-
-module Proofview_monad :
-sig
- type lazy_msg = unit -> Pp.t
- module Info :
- sig
- type tree
- end
-end
-
-module Evarutil :
-sig
- val e_new_global : Evd.evar_map ref -> Globnames.global_reference -> EConstr.constr
-
- val nf_evars_and_universes : Evd.evar_map -> Evd.evar_map * (Constr.t -> Constr.t)
- val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
- val nf_evar_info : Evd.evar_map -> Evd.evar_info -> Evd.evar_info
-
- val mk_new_meta : unit -> EConstr.constr
-
- (** [new_meta] is a generator of unique meta variables *)
- val new_meta : unit -> Constr.metavariable
-
- val new_Type : ?rigid:Evd.rigid -> Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.constr
- val new_global : Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * EConstr.constr
-
- val new_evar :
- Environ.env -> Evd.evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t ->
- ?candidates:EConstr.constr list -> ?store:Evd.Store.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool -> EConstr.types -> Evd.evar_map * EConstr.constr
-
- val new_evar_instance :
- Environ.named_context_val -> Evd.evar_map -> EConstr.types ->
- ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list ->
- ?store:Evd.Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool ->
- EConstr.constr list -> Evd.evar_map * EConstr.constr
-
- val clear_hyps_in_evi : Environ.env -> Evd.evar_map ref -> Environ.named_context_val ->
- EConstr.types -> Names.Id.Set.t -> Environ.named_context_val * EConstr.types
-
- type clear_dependency_error =
- | OccurHypInSimpleClause of Names.Id.t option
- | EvarTypingBreak of Constr.existential
-
- exception ClearDependencyError of Names.Id.t * clear_dependency_error
- val undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t
- val has_undefined_evars : Evd.evar_map -> EConstr.constr -> bool
- val e_new_evar :
- Environ.env -> Evd.evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t ->
- ?candidates:EConstr.constr list -> ?store:Evd.Store.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool -> EConstr.types -> EConstr.constr
- val new_type_evar :
- Environ.env -> Evd.evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> Evd.rigid ->
- Evd.evar_map * (EConstr.constr * Sorts.t)
- val nf_evars_universes : Evd.evar_map -> Constr.t -> Constr.t
- val safe_evar_value : Evd.evar_map -> Constr.existential -> Constr.t option
- val evd_comb1 : (Evd.evar_map -> 'b -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'b -> 'a
-end
-
-module Proofview :
-sig
- type proofview
- type entry
- type +'a tactic
- type telescope =
- | TNil of Evd.evar_map
- | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
-
- module NonLogical :
- sig
- type +'a t
- val make : (unit -> 'a) -> 'a t
- val return : 'a -> 'a t
- val ( >> ) : unit t -> 'a t -> 'a t
- val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t
- val print_char : char -> unit t
- val print_debug : Pp.t -> unit t
- val print_warning : Pp.t -> unit t
- val print_notice : Pp.t -> unit t
- val print_info : Pp.t -> unit t
- val run : 'a t -> 'a
- type 'a ref
- val ref : 'a -> 'a ref t
- val ( := ) : 'a ref -> 'a -> unit t
- val ( ! ) : 'a ref -> 'a t
- val raise : ?info:Exninfo.info -> exn -> 'a t
- val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
- val read_line : string t
- end
- val proofview : proofview -> Evar.t list * Evd.evar_map
- val cycle : int -> unit tactic
- val swap : int -> int -> unit tactic
- val revgoals : unit tactic
- val give_up : unit tactic
- val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofview
- val shelve : unit tactic
- val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
- val tclUNIT : 'a -> 'a tactic
- val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
- val tclORELSE : 'a tactic -> (Util.iexn -> 'a tactic) -> 'a tactic
- val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
- val tclEVARMAP : Evd.evar_map tactic
- val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
- val tclLIFT : 'a NonLogical.t -> 'a tactic
- val tclOR : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
- val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic
- val tclINDEPENDENT : unit tactic -> unit tactic
- val tclDISPATCH : unit tactic list -> unit tactic
- val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
- val tclBREAK : (Exninfo.iexn -> Exninfo.iexn option) -> 'a tactic -> 'a tactic
- val tclENV : Environ.env tactic
- val tclONCE : 'a tactic -> 'a tactic
- val tclPROGRESS : 'a tactic -> 'a tactic
- val shelve_unifiable : unit tactic
- val apply : Environ.env -> 'a tactic -> proofview -> 'a
- * proofview
- * (bool * Evar.t list * Evar.t list)
- * Proofview_monad.Info.tree
- val numgoals : int tactic
- val with_shelf : 'a tactic -> (Evar.t list * 'a) tactic
-
- module Unsafe :
- sig
- val tclEVARS : Evd.evar_map -> unit tactic
-
- val tclGETGOALS : Evar.t list tactic
-
- val tclSETGOALS : Evar.t list -> unit tactic
-
- val tclNEWGOALS : Evar.t list -> unit tactic
- end
-
- module Goal :
- sig
- type 'a t
- val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
- val hyps : 'a t -> EConstr.named_context
- val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic
- val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic
- val concl : 'a t -> EConstr.constr
- val sigma : 'a t -> Evd.evar_map
- val goal : [ `NF ] t -> Evar.t
- val env : 'a t -> Environ.env
- val assume : 'a t -> [ `NF ] t
- end
-
- module Notations :
- sig
- val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
- val (<*>) : unit tactic -> 'a tactic -> 'a tactic
- val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
- end
- module V82 :
- sig
- type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
-
- val tactic : tac -> unit tactic
-
- val of_tactic : 'a tactic -> tac
-
- val nf_evar_goals : unit tactic
-
- val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic
-
- val catchable_exception : exn -> bool
- end
- module Trace :
- sig
- val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
- val log : Proofview_monad.lazy_msg -> unit tactic
- end
-end
-
-module Ftactic :
-sig
- type +'a focus
- type +'a t = 'a focus Proofview.tactic
- val return : 'a -> 'a t
- val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
- val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t
- val nf_enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t
- val bind : 'a t -> ('a -> 'b t) -> 'b t
- val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
- val lift : 'a Proofview.tactic -> 'a t
- val with_env : 'a t -> (Environ.env * 'a) t
- module List :
- sig
- val map : ('a -> 'b t) -> 'a list -> 'b list t
- val map_right : ('a -> 'b t) -> 'a list -> 'b list t
- end
- module Notations :
- sig
- val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
- val (<*>) : unit t -> 'a t -> 'a t
- end
-end
-
-module Geninterp :
-sig
- module Val :
- sig
- type 'a typ
- type t = Dyn : 'a typ * 'a -> t
- type 'a tag =
- | Base : 'a typ -> 'a tag
- | List : 'a tag -> 'a list tag
- | Opt : 'a tag -> 'a option tag
- | Pair : 'a tag * 'b tag -> ('a * 'b) tag
- val create : string -> 'a typ
- val pr : 'a typ -> Pp.t
- val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
- val typ_list : t list typ
- val typ_opt : t option typ
- val typ_pair : (t * t) typ
- val repr : 'a typ -> string
- val inject : 'a tag -> 'a -> t
- end
- module TacStore :
- sig
- type t
- type 'a field
- val empty : t
- val field : unit -> 'a field
- val get : t -> 'a field -> 'a option
- val set : t -> 'a field -> 'a -> t
- val remove : t -> 'a field -> t
- val merge : t -> t -> t
- end
- type interp_sign = {
- lfun : Val.t Names.Id.Map.t;
- extra : TacStore.t
- }
- type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
- val register_interp0 :
- ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun -> unit
- val register_val0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'top Val.tag option -> unit
- val val_tag : 'a Genarg.typed_abstract_argument_type -> 'a Val.tag
- val interp : ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun
-end
-
-(************************************************************************)
-(* End of modules from engine/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from pretyping/ *)
-(************************************************************************)
-
-module Ltac_pretype :
-sig
-open Names
-open Glob_term
-
-(** {5 Maps of pattern variables} *)
-
-(** Type [constr_under_binders] is for representing the term resulting
- of a matching. Matching can return terms defined in a some context
- of named binders; in the context, variable names are ordered by
- (<) and referred to by index in the term Thanks to the canonical
- ordering, a matching problem like
-
- [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
-
- will be accepted. Thanks to the reference by index, a matching
- problem like
-
- [match ... with [(fun x => ?p)] => [forall x => p]]
-
- will work even if [x] is also the name of an existing goal
- variable.
-
- Note: we do not keep types in the signature. Besides simplicity,
- the main reason is that it would force to close the signature over
- binders that occur only in the types of effective binders but not
- in the term itself (e.g. for a term [f x] with [f:A -> True] and
- [x:A]).
-
- On the opposite side, by not keeping the types, we loose
- opportunity to propagate type informations which otherwise would
- not be inferable, as e.g. when matching [forall x, x = 0] with
- pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
- expression [forall x, h = x] where nothing tells how the type of x
- could be inferred. We also loose the ability of typing ltac
- variables before calling the right-hand-side of ltac matching clauses. *)
-
-type constr_under_binders = Id.t list * EConstr.constr
-
-(** Types of substitutions with or w/o bound variables *)
-
-type patvar_map = EConstr.constr Id.Map.t
-type extended_patvar_map = constr_under_binders Id.Map.t
-
-(** A globalised term together with a closure representing the value
- of its free variables. Intended for use when these variables are taken
- from the Ltac environment. *)
-type closure = {
- idents:Id.t Id.Map.t;
- typed: constr_under_binders Id.Map.t ;
- untyped:closed_glob_constr Id.Map.t }
-and closed_glob_constr = {
- closure: closure;
- term: glob_constr }
-
-(** Ltac variable maps *)
-type var_map = constr_under_binders Id.Map.t
-type uconstr_var_map = closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
-
-type ltac_var_map = {
- ltac_constrs : var_map;
- (** Ltac variables bound to constrs *)
- ltac_uconstrs : uconstr_var_map;
- (** Ltac variables bound to untyped constrs *)
- ltac_idents: Id.t Id.Map.t;
- (** Ltac variables bound to identifiers *)
- ltac_genargs : unbound_ltac_var_map;
- (** Ltac variables bound to other kinds of arguments *)
-}
-
-end
-
-module Locusops :
-sig
- val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool
- val nowhere : 'a Locus.clause_expr
- val allHypsAndConcl : 'a Locus.clause_expr
- val is_nowhere : 'a Locus.clause_expr -> bool
- val occurrences_map :
- ('a list -> 'b list) -> 'a Locus.occurrences_gen -> 'b Locus.occurrences_gen
- val convert_occs : Locus.occurrences -> bool * int list
- val onConcl : 'a Locus.clause_expr
- val onHyp : 'a -> 'a Locus.clause_expr
-end
-
-module Pretype_errors :
-sig
- type unification_error
- type subterm_unification_error
-
- type type_error = (EConstr.t, EConstr.types) Type_errors.ptype_error
-
- type pretype_error =
- | CantFindCaseType of EConstr.constr
- | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
- | UnifOccurCheck of Evar.t * EConstr.constr
- | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option
- | CannotUnify of EConstr.constr * EConstr.constr * unification_error option
- | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr
- | CannotUnifyBindingType of EConstr.constr * EConstr.constr
- | CannotGeneralize of EConstr.constr
- | NoOccurrenceFound of EConstr.constr * Names.Id.t option
- | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (Environ.env * type_error) option
- | WrongAbstractionType of Names.Name.t * EConstr.constr * EConstr.types * EConstr.types
- | AbstractionOverMeta of Names.Name.t * Names.Name.t
- | NonLinearUnification of Names.Name.t * EConstr.constr
- | VarNotFound of Names.Id.t
- | UnexpectedType of EConstr.constr * EConstr.constr
- | NotProduct of EConstr.constr
- | TypingError of type_error
- | CannotUnifyOccurrences of subterm_unification_error
- | UnsatisfiableConstraints of
- (Evar.t * Evar_kinds.t) option * Evar.Set.t option
-
- exception PretypeError of Environ.env * Evd.evar_map * pretype_error
- val error_var_not_found : ?loc:Loc.t -> Names.Id.t -> 'b
- val precatchable_exception : exn -> bool
-end
-
-module Reductionops :
-sig
- type local_reduction_function = Evd.evar_map -> EConstr.constr -> EConstr.constr
-
- type reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
-
- type local_stack_reduction_function =
- Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr list
-
- type e_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
- type state
-
- val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function
- val nf_beta : local_reduction_function
- val nf_betaiota : local_reduction_function
- val splay_prod : Environ.env -> Evd.evar_map -> EConstr.constr ->
- (Names.Name.t * EConstr.constr) list * EConstr.constr
- val splay_prod_n : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.rel_context * EConstr.constr
- val whd_all : reduction_function
- val whd_beta : local_reduction_function
-
- val whd_betaiotazeta : local_reduction_function
-
- val whd_betaiota_stack : local_stack_reduction_function
-
- val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
- val is_conv : ?reds:Names.transparent_state -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
- val beta_applist : Evd.evar_map -> EConstr.constr * EConstr.constr list -> EConstr.constr
- val sort_of_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.ESorts.t
- val is_conv_leq : ?reds:Names.transparent_state -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
- val whd_betaiota : local_reduction_function
- val is_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
- val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
- val nf_meta : Evd.evar_map -> EConstr.constr -> EConstr.constr
- val hnf_prod_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr
- val pr_state : state -> Pp.t
- module Stack :
- sig
- type 'a t
- val pr : ('a -> Pp.t) -> 'a t -> Pp.t
- end
- module Cst_stack :
- sig
- type t
- val pr : t -> Pp.t
- end
-end
-
-module Inductiveops :
-sig
- type inductive_family
- type inductive_type =
- | IndType of inductive_family * EConstr.constr list
- type constructor_summary =
- {
- cs_cstr : Constr.pconstructor;
- cs_params : Constr.t list;
- cs_nargs : int;
- cs_args : Context.Rel.t;
- cs_concl_realargs : Constr.t array;
- }
-
- val arities_of_constructors : Environ.env -> Constr.pinductive -> Constr.types array
- val constructors_nrealargs_env : Environ.env -> Names.inductive -> int array
- val constructor_nallargs_env : Environ.env -> Names.constructor -> int
-
- val inductive_nparams : Names.inductive -> int
-
- val inductive_nparamdecls : Names.inductive -> int
-
- val type_of_constructors : Environ.env -> Constr.pinductive -> Constr.types array
- val find_mrectype : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.constr list
- val mis_is_recursive :
- Names.inductive * Declarations.mutual_inductive_body * Declarations.one_inductive_body -> bool
- val nconstructors : Names.inductive -> int
- val find_rectype : Environ.env -> Evd.evar_map -> EConstr.types -> inductive_type
- val get_constructors : Environ.env -> inductive_family -> constructor_summary array
- val dest_ind_family : inductive_family -> Names.inductive Univ.puniverses * Constr.t list
- val find_inductive : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * Constr.t list
- val type_of_inductive : Environ.env -> Constr.pinductive -> Constr.types
-end
-
-module Impargs :
-sig
- type implicit_status
- type implicit_side_condition
- type implicits_list = implicit_side_condition * implicit_status list
- type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
- type manual_implicits = manual_explicitation list
- val is_status_implicit : implicit_status -> bool
- val name_of_implicit : implicit_status -> Names.Id.t
- val implicits_of_global : Globnames.global_reference -> implicits_list list
- val declare_manual_implicits : bool -> Globnames.global_reference -> ?enriching:bool ->
- manual_implicits list -> unit
- val is_implicit_args : unit -> bool
- val is_strict_implicit_args : unit -> bool
- val is_contextual_implicit_args : unit -> bool
- val make_implicit_args : bool -> unit
- val make_strict_implicit_args : bool -> unit
- val make_contextual_implicit_args : bool -> unit
-end
-
-module Retyping : (* reconstruct the type of a term knowing that it was already typechecked *)
-sig
- val get_type_of : ?polyprop:bool -> ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types
- val get_sort_family_of : ?truncation_style:bool -> ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family
- val expand_projection : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.constr -> EConstr.constr list -> EConstr.constr
- val get_sort_of :
- ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.t
-end
-
-module Find_subterm :
-sig
- val error_invalid_occurrence : int list -> 'a
-end
-
-module Evarsolve :
-sig
- val refresh_universes :
- ?status:Evd.rigid -> ?onlyalg:bool -> ?refreshset:bool -> bool option ->
- Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.types
-end
-
-module Recordops :
-sig
-
- type cs_pattern =
- | Const_cs of Globnames.global_reference
- | Prod_cs
- | Sort_cs of Sorts.family
- | Default_cs
-
- type obj_typ = {
- o_DEF : Constr.t;
- o_CTX : Univ.AUContext.t;
- o_INJ : int option; (** position of trivial argument *)
- o_TABS : Constr.t list; (** ordered *)
- o_TPARAMS : Constr.t list; (** ordered *)
- o_NPARAMS : int;
- o_TCOMPS : Constr.t list }
-
- val lookup_projections : Names.inductive -> Names.Constant.t option list
- val lookup_canonical_conversion : (Globnames.global_reference * cs_pattern) -> Constr.t * obj_typ
- val find_projection_nparams : Globnames.global_reference -> int
-end
-
-module Evarconv :
-sig
- val e_conv : Environ.env -> ?ts:Names.transparent_state -> Evd.evar_map ref -> EConstr.constr -> EConstr.constr -> bool
- val the_conv_x : Environ.env -> ?ts:Names.transparent_state -> EConstr.constr -> EConstr.constr -> Evd.evar_map -> Evd.evar_map
- val the_conv_x_leq : Environ.env -> ?ts:Names.transparent_state -> EConstr.constr -> EConstr.constr -> Evd.evar_map -> Evd.evar_map
- val solve_unif_constraints_with_heuristics : Environ.env -> ?ts:Names.transparent_state -> Evd.evar_map -> Evd.evar_map
-end
-
-module Typing :
-sig
- val e_sort_of : Environ.env -> Evd.evar_map ref -> EConstr.types -> Sorts.t
-
- val type_of : ?refresh:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types
- val e_solve_evars : Environ.env -> Evd.evar_map ref -> EConstr.constr -> EConstr.constr
-
- val unsafe_type_of : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types
-
- val e_check : Environ.env -> Evd.evar_map ref -> EConstr.constr -> EConstr.types -> unit
-
- val e_type_of : ?refresh:bool -> Environ.env -> Evd.evar_map ref -> EConstr.constr -> EConstr.types
-end
-
-module Miscops :
-sig
- val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
- ('a,'b,'c) Genredexpr.red_expr_gen -> ('d,'e,'f) Genredexpr.red_expr_gen
- val map_cast_type : ('a -> 'b) -> 'a Misctypes.cast_type -> 'b Misctypes.cast_type
-end
-
-module Glob_ops :
-sig
- val map_glob_constr_left_to_right : (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr
- val loc_of_glob_constr : Glob_term.glob_constr -> Loc.t option
- val glob_constr_eq : Glob_term.glob_constr -> Glob_term.glob_constr -> bool
- val bound_glob_vars : Glob_term.glob_constr -> Names.Id.Set.t
-
- (** Conversion from glob_constr to cases pattern, if possible
-
- Take the current alias as parameter,
- @raise Not_found if translation is impossible *)
- val cases_pattern_of_glob_constr : Names.Name.t -> Glob_term.glob_constr -> Glob_term.cases_pattern
- val map_glob_constr :
- (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr
-
- val empty_lvar : Ltac_pretype.ltac_var_map
-
-end
-
-module Redops :
-sig
- val all_flags : 'a Genredexpr.glob_red_flag
- val make_red_flag : 'a Genredexpr.red_atom list -> 'a Genredexpr.glob_red_flag
-end
-
-module Patternops :
-sig
- val pattern_of_glob_constr : Glob_term.glob_constr -> Names.Id.t list * Pattern.constr_pattern
- val subst_pattern : Mod_subst.substitution -> Pattern.constr_pattern -> Pattern.constr_pattern
- val pattern_of_constr : Environ.env -> Evd.evar_map -> Constr.t -> Pattern.constr_pattern
- val instantiate_pattern : Environ.env ->
- Evd.evar_map -> Ltac_pretype.extended_patvar_map ->
- Pattern.constr_pattern -> Pattern.constr_pattern
-end
-
-module Constr_matching :
-sig
- val special_meta : Constr.metavariable
-
- type binding_bound_vars = Names.Id.Set.t
- type bound_ident_map = Names.Id.t Names.Id.Map.t
- val is_matching : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> bool
- val extended_matches :
- Environ.env -> Evd.evar_map -> binding_bound_vars * Pattern.constr_pattern ->
- EConstr.constr -> bound_ident_map * Ltac_pretype.extended_patvar_map
- exception PatternMatchingFailure
- type matching_result =
- { m_sub : bound_ident_map * Ltac_pretype.patvar_map;
- m_ctx : EConstr.constr }
- val match_subterm : Environ.env -> Evd.evar_map ->
- binding_bound_vars * Pattern.constr_pattern -> EConstr.constr ->
- matching_result IStream.t
- val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map
-end
-
-module Tacred :
-sig
- val try_red_product : Reductionops.reduction_function
- val simpl : Reductionops.reduction_function
- val unfoldn :
- (Locus.occurrences * Names.evaluable_global_reference) list -> Reductionops.reduction_function
- val hnf_constr : Reductionops.reduction_function
- val red_product : Reductionops.reduction_function
- val is_evaluable : Environ.env -> Names.evaluable_global_reference -> bool
- val evaluable_of_global_reference :
- Environ.env -> Globnames.global_reference -> Names.evaluable_global_reference
- val error_not_evaluable : Globnames.global_reference -> 'a
- val reduce_to_quantified_ref :
- Environ.env -> Evd.evar_map -> Globnames.global_reference -> EConstr.types -> EConstr.types
- val pattern_occs : (Locus.occurrences * EConstr.constr) list -> Reductionops.e_reduction_function
- val cbv_norm_flags : CClosure.RedFlags.reds -> Reductionops.reduction_function
-end
-
-(* XXX: Located manually from intf *)
-module Tok :
-sig
-
- type t =
- | KEYWORD of string
- | PATTERNIDENT of string
- | IDENT of string
- | FIELD of string
- | INT of string
- | STRING of string
- | LEFTQMARK
- | BULLET of string
- | EOI
-
-end
-
-module CLexer :
-sig
- val add_keyword : string -> unit
- val remove_keyword : string -> unit
- val is_keyword : string -> bool
- val keywords : unit -> CString.Set.t
-
- type keyword_state
- val set_keyword_state : keyword_state -> unit
- val get_keyword_state : unit -> keyword_state
-
- val check_ident : string -> unit
- val terminal : string -> Tok.t
-
- include Grammar.GLexerType with type te = Tok.t
-end
-
-module Extend :
-sig
-
- type gram_assoc = NonA | RightA | LeftA
-
- type gram_position =
- | First
- | Last
- | Before of string
- | After of string
- | Level of string
-
- type production_level =
- | NextLevel
- | NumLevel of int
-
- type 'a entry = 'a Grammar.GMake(CLexer).Entry.e
-
- type 'a user_symbol =
- | Ulist1 of 'a user_symbol
- | Ulist1sep of 'a user_symbol * string
- | Ulist0 of 'a user_symbol
- | Ulist0sep of 'a user_symbol * string
- | Uopt of 'a user_symbol
- | Uentry of 'a
- | Uentryl of 'a * int
-
- type ('self, 'a) symbol =
- | Atoken : Tok.t -> ('self, string) symbol
- | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol
- | Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
- | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol
- | Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
- | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol
- | Aself : ('self, 'self) symbol
- | Anext : ('self, 'self) symbol
- | Aentry : 'a entry -> ('self, 'a) symbol
- | Aentryl : 'a entry * int -> ('self, 'a) symbol
- | Arules : 'a rules list -> ('self, 'a) symbol
-
- and ('self, _, 'r) rule =
- | Stop : ('self, 'r, 'r) rule
- | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule
-
- and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule }
-
- and 'a rules =
- | Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules
-
- type ('lev,'pos) constr_entry_key_gen =
- | ETName | ETReference | ETBigint
- | ETBinder of bool
- | ETConstr of ('lev * 'pos)
- | ETPattern
- | ETOther of string * string
- | ETConstrList of ('lev * 'pos) * Tok.t list
- | ETBinderList of bool * Tok.t list
-
- type side = Left | Right
-
- type production_position =
- | BorderProd of side * gram_assoc option
- | InternalProd
-
- type constr_prod_entry_key =
- (production_level,production_position) constr_entry_key_gen
-
- type simple_constr_prod_entry_key =
- (production_level,unit) constr_entry_key_gen
-
- type 'a production_rule =
- | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
-
- type 'a single_extend_statment =
- string option *
- (** Level *)
- gram_assoc option *
- (** Associativity *)
- 'a production_rule list
- (** Symbol list with the interpretation function *)
-
- type 'a extend_statment =
- gram_position option *
- 'a single_extend_statment list
-end
-
-(* XXX: Located manually from intf *)
-module Vernacexpr :
-sig
- open Misctypes
- open Constrexpr
- open Libnames
-
- type instance_flag = bool option
- type coercion_flag = bool
- type inductive_flag = Declarations.recursivity_kind
- type lname = Names.Name.t Loc.located
- type lident = Names.Id.t Loc.located
- type opacity_flag =
- | Opaque
- | Transparent
- type locality_flag = bool
- type inductive_kind =
- | Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool
-
- type vernac_type =
- | VtStartProof of vernac_start
- | VtSideff of vernac_sideff_type
- | VtQed of vernac_qed_type
- | VtProofStep of proof_step
- | VtProofMode of string
- | VtQuery of vernac_part_of_script * Feedback.route_id
- | VtMeta
- | VtUnknown
- and vernac_qed_type =
- | VtKeep
- | VtKeepAsAxiom
- | VtDrop
- and vernac_start = string * opacity_guarantee * Names.Id.t list
- and vernac_sideff_type = Names.Id.t list
- and vernac_part_of_script = bool
- and opacity_guarantee =
- | GuaranteesOpacity
- | Doesn'tGuaranteeOpacity
- and proof_step = {
- parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
- proof_block_detection : proof_block_name option
- }
- and solving_tac = bool
- and anon_abstracting_tac = bool
- and proof_block_name = string
-
- type vernac_when =
- | VtNow
- | VtLater
-
- type verbose_flag = bool
-
- type universe_decl_expr = (lident list, Misctypes.glob_constraint list) gen_universe_decl
-
- type ident_decl = lident * universe_decl_expr option
-
- type lstring
- type 'a with_coercion = coercion_flag * 'a
- type scope_name = string
- type decl_notation = lstring * Constrexpr.constr_expr * scope_name option
- type constructor_expr = (lident * Constrexpr.constr_expr) with_coercion
- type 'a with_notation = 'a * decl_notation list
-
- type local_decl_expr =
- | AssumExpr of lname * Constrexpr.constr_expr
- | DefExpr of lname * Constrexpr.constr_expr * Constrexpr.constr_expr option
-
- type 'a with_priority = 'a * int option
- type 'a with_instance = instance_flag * 'a
- type constructor_list_or_record_decl_expr =
- | Constructors of constructor_expr list
- | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
-
- type inductive_expr = ident_decl with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr
-
- type syntax_modifier =
- | SetItemLevel of string list * Extend.production_level
- | SetLevel of int
- | SetAssoc of Extend.gram_assoc
- | SetEntryType of string * Extend.simple_constr_prod_entry_key
- | SetOnlyParsing
- | SetOnlyPrinting
- | SetCompatVersion of Flags.compat_version
- | SetFormat of string * string Loc.located
-
- type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
-
- type typeclass_constraint = (Names.Name.t Loc.located * universe_decl_expr option) * Decl_kinds.binding_kind * constr_expr
-
- type definition_expr =
- | ProveBody of local_binder_expr list * constr_expr
- | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
- * constr_expr option
- type proof_expr =
- ident_decl option * (local_binder_expr list * constr_expr)
-
- type proof_end =
- | Admitted
- | Proved of opacity_flag * lident option
-
- type fixpoint_expr = ident_decl * (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option
-
- type cofixpoint_expr
-
- type scheme
-
- type section_subset_expr
-
- type module_binder
-
- type vernac_argument_status
- type vernac_implicit_status
- type module_ast_inl
- type extend_name = string * int
- type simple_binder
- type option_value
- type showable
- type bullet
- type comment
- type register_kind
- type locatable
- type search_restriction
- type searchable
- type printable
- type option_ref_value
- type onlyparsing_flag
- type reference_or_constr
-
- type hint_mode
-
- type 'a hint_info_gen =
- { hint_priority : int option;
- hint_pattern : 'a option }
-
- type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
-
- type hints_expr =
- | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
- | HintsImmediate of reference_or_constr list
- | HintsUnfold of Libnames.reference list
- | HintsTransparency of Libnames.reference list * bool
- | HintsMode of Libnames.reference * hint_mode list
- | HintsConstructors of Libnames.reference list
- | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
- type 'a module_signature =
- | Enforce of 'a (** ... : T *)
- | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
-
- type inline =
- | NoInline
- | DefaultInline
- | InlineAt of int
-
- type cumulative_inductive_parsing_flag =
- | GlobalCumulativity
- | GlobalNonCumulativity
- | LocalCumulativity
- | LocalNonCumulativity
-
- type vernac_expr =
- | VernacLoad of verbose_flag * string
- | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
- | VernacOpenCloseScope of bool * scope_name
- | VernacDelimiters of scope_name * string option
- | VernacBindScope of scope_name * class_rawexpr list
- | VernacInfix of (lstring * syntax_modifier list) *
- Constrexpr.constr_expr * scope_name option
- | VernacNotation of
- Constrexpr.constr_expr * (lstring * syntax_modifier list) *
- scope_name option
- | VernacNotationAddFormat of string * string * string
- | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * ident_decl * definition_expr
- | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
- | VernacEndProof of proof_end
- | VernacExactProof of Constrexpr.constr_expr
- | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
- inline * (ident_decl list * Constrexpr.constr_expr) with_coercion list
- | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
- | VernacFixpoint of
- Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
- | VernacCoFixpoint of
- Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
- | VernacScheme of (lident option * scheme) list
- | VernacCombinedScheme of lident * lident list
- | VernacUniverse of lident list
- | VernacConstraint of (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list
- | VernacBeginSection of lident
- | VernacEndSegment of lident
- | VernacRequire of
- Libnames.reference option * bool option * Libnames.reference list
- | VernacImport of bool * Libnames.reference list
- | VernacCanonical of Libnames.reference Misctypes.or_by_notation
- | VernacCoercion of Libnames.reference Misctypes.or_by_notation *
- class_rawexpr * class_rawexpr
- | VernacIdentityCoercion of lident *
- class_rawexpr * class_rawexpr
- | VernacNameSectionHypSet of lident * section_subset_expr
- | VernacInstance of
- bool *
- Constrexpr.local_binder_expr list *
- typeclass_constraint *
- (bool * Constrexpr.constr_expr) option *
- hint_info_expr
- | VernacContext of Constrexpr.local_binder_expr list
- | VernacDeclareInstances of
- (Libnames.reference * hint_info_expr) list
- | VernacDeclareClass of Libnames.reference
- | VernacDeclareModule of bool option * lident *
- module_binder list * module_ast_inl
- | VernacDefineModule of bool option * lident * module_binder list *
- module_ast_inl module_signature * module_ast_inl list
- | VernacDeclareModuleType of lident *
- module_binder list * module_ast_inl list * module_ast_inl list
- | VernacInclude of module_ast_inl list
- | VernacSolveExistential of int * Constrexpr.constr_expr
- | VernacAddLoadPath of bool * string * Names.DirPath.t option
- | VernacRemoveLoadPath of string
- | VernacAddMLPath of bool * string
- | VernacDeclareMLModule of string list
- | VernacChdir of string option
- | VernacWriteState of string
- | VernacRestoreState of string
- | VernacResetName of lident
- | VernacResetInitial
- | VernacBack of int
- | VernacBackTo of int
- | VernacCreateHintDb of string * bool
- | VernacRemoveHints of string list * Libnames.reference list
- | VernacHints of string list * hints_expr
- | VernacSyntacticDefinition of Names.Id.t Loc.located * (Names.Id.t list * Constrexpr.constr_expr) *
- onlyparsing_flag
- | VernacDeclareImplicits of Libnames.reference Misctypes.or_by_notation *
- (Constrexpr.explicitation * bool * bool) list list
- | VernacArguments of Libnames.reference Misctypes.or_by_notation *
- vernac_argument_status list *
- (Names.Name.t * vernac_implicit_status) list list *
- int option *
- [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
- `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
- `DefaultImplicits ] list
- | VernacArgumentsScope of Libnames.reference Misctypes.or_by_notation *
- scope_name option list
- | VernacReserve of simple_binder list
- | VernacGeneralizable of (lident list) option
- | VernacSetOpacity of (Conv_oracle.level * Libnames.reference Misctypes.or_by_notation list)
- | VernacSetStrategy of
- (Conv_oracle.level * Libnames.reference Misctypes.or_by_notation list) list
- | VernacUnsetOption of Goptions.option_name
- | VernacSetOption of Goptions.option_name * option_value
- | VernacSetAppendOption of Goptions.option_name * string
- | VernacAddOption of Goptions.option_name * option_ref_value list
- | VernacRemoveOption of Goptions.option_name * option_ref_value list
- | VernacMemOption of Goptions.option_name * option_ref_value list
- | VernacPrintOption of Goptions.option_name
- | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * Constrexpr.constr_expr
- | VernacGlobalCheck of Constrexpr.constr_expr
- | VernacDeclareReduction of string * Genredexpr.raw_red_expr
- | VernacPrint of printable
- | VernacSearch of searchable * goal_selector option * search_restriction
- | VernacLocate of locatable
- | VernacRegister of lident * register_kind
- | VernacComments of comment list
- | VernacGoal of Constrexpr.constr_expr
- | VernacAbort of lident option
- | VernacAbortAll
- | VernacRestart
- | VernacUndo of int
- | VernacUndoTo of int
- | VernacBacktrack of int*int*int
- | VernacFocus of int option
- | VernacUnfocus
- | VernacUnfocused
- | VernacBullet of bullet
- | VernacSubproof of int option
- | VernacEndSubproof
- | VernacShow of showable
- | VernacCheckGuard
- | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
- | VernacProofMode of string
- | VernacToplevelControl of exn
- | VernacExtend of extend_name * Genarg.raw_generic_argument list
- | VernacProgram of vernac_expr
- | VernacPolymorphic of bool * vernac_expr
- | VernacLocal of bool * vernac_expr
- and goal_selector =
- | SelectNth of int
- | SelectList of (int * int) list
- | SelectId of Names.Id.t
- | SelectAll
- and vernac_classification = vernac_type * vernac_when
- and one_inductive_expr =
- ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list
-
-type vernac_control =
- | VernacExpr of vernac_expr
- (* Control *)
- | VernacTime of bool * vernac_control Loc.located
- | VernacRedirect of string * vernac_control Loc.located
- | VernacTimeout of int * vernac_control
- | VernacFail of vernac_control
-
-
-end
-(* XXX: end of moved from intf *)
-
-module Typeclasses :
-sig
- type typeclass = {
- cl_univs : Univ.AUContext.t;
- cl_impl : Globnames.global_reference;
- cl_context : Globnames.global_reference option list * Context.Rel.t;
- cl_props : Context.Rel.t;
- cl_projs : (Names.Name.t * (direction * Vernacexpr.hint_info_expr) option
- * Names.Constant.t option) list;
- cl_strict : bool;
- cl_unique : bool;
- }
- and direction
-
- type instance
- type evar_filter = Evar.t -> Evar_kinds.t -> bool
-
- val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
- ?split:bool -> ?fail:bool -> Environ.env -> Evd.evar_map -> Evd.evar_map
- val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t
- val resolve_one_typeclass : ?unique:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.constr
- val class_info : Globnames.global_reference -> typeclass
- val mark_resolvables : ?filter:evar_filter -> Evd.evar_map -> Evd.evar_map
- val add_instance : instance -> unit
- val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool ->
- Globnames.global_reference -> instance
-end
-
-module Classops :
-sig
- type coe_index
- type inheritance_path = coe_index list
- type cl_index
-
- val hide_coercion : Globnames.global_reference -> int option
- val lookup_path_to_sort_from : Environ.env -> Evd.evar_map -> EConstr.types ->
- EConstr.types * inheritance_path
- val get_coercion_value : coe_index -> Constr.t
- val coercions : unit -> coe_index list
- val pr_cl_index : cl_index -> Pp.t
-end
-
-module Detyping :
-sig
- type 'a delay =
- | Now : 'a delay
- | Later : [ `thunk ] delay
- val print_universes : bool ref
- val print_evar_arguments : bool ref
- val print_allow_match_default_clause : bool ref
- val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g
- val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr
- val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit
-end
-
-module Indrec :
-sig
- type dep_flag = bool
- val lookup_eliminator : Names.inductive -> Sorts.family -> Globnames.global_reference
- val build_case_analysis_scheme : Environ.env -> Evd.evar_map -> Constr.pinductive ->
- dep_flag -> Sorts.family -> Evd.evar_map * Constr.t
- val make_elimination_ident : Names.Id.t -> Sorts.family -> Names.Id.t
- val build_mutual_induction_scheme :
- Environ.env -> Evd.evar_map -> (Constr.pinductive * dep_flag * Sorts.family) list -> Evd.evar_map * Constr.t list
- val build_case_analysis_scheme_default : Environ.env -> Evd.evar_map -> Constr.pinductive ->
- Sorts.family -> Evd.evar_map * Constr.t
-end
-
-module Pretyping :
-sig
- type typing_constraint =
- | OfType of EConstr.types
- | IsType
- | WithoutTypeConstraint
-
- type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> Evd.evar_map * EConstr.constr
-
- type inference_flags = {
- use_typeclasses : bool;
- solve_unification_constraints : bool;
- use_hook : inference_hook option;
- fail_evar : bool;
- expand_evars : bool
- }
-
- val understand_ltac : inference_flags ->
- Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map ->
- typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t
- val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map ->
- ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
- val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
- Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Constr.t Evd.in_evar_universe_context
- val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit
- val register_constr_interp0 :
- ('r, 'g, 't) Genarg.genarg_type ->
- (Ltac_pretype.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit
- val all_and_fail_flags : inference_flags
- val ise_pretype_gen :
- inference_flags -> Environ.env -> Evd.evar_map ->
- Ltac_pretype.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
-end
-
-module Unification :
-sig
- type core_unify_flags = {
- modulo_conv_on_closed_terms : Names.transparent_state option;
- use_metas_eagerly_in_conv_on_closed_terms : bool;
- use_evars_eagerly_in_conv_on_closed_terms : bool;
- modulo_delta : Names.transparent_state;
- modulo_delta_types : Names.transparent_state;
- check_applied_meta_types : bool;
- use_pattern_unification : bool;
- use_meta_bound_pattern_unification : bool;
- frozen_evars : Evar.Set.t;
- restrict_conv_on_strict_subterms : bool;
- modulo_betaiota : bool;
- modulo_eta : bool;
- }
- type unify_flags =
- {
- core_unify_flags : core_unify_flags;
- merge_unify_flags : core_unify_flags;
- subterm_unify_flags : core_unify_flags;
- allow_K_in_toplevel_higher_order_unification : bool;
- resolve_evars : bool
- }
- val default_no_delta_unify_flags : unit -> unify_flags
- val w_unify : Environ.env -> Evd.evar_map -> Reduction.conv_pb -> ?flags:unify_flags -> EConstr.constr -> EConstr.constr -> Evd.evar_map
- val elim_flags : unit -> unify_flags
- val w_unify_to_subterm :
- Environ.env -> Evd.evar_map -> ?flags:unify_flags -> EConstr.constr * EConstr.constr -> Evd.evar_map * EConstr.constr
-end
-
-module Univdecls :
-sig
- type universe_decl =
- (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
- val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr ->
- Evd.evar_map * universe_decl
- val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option ->
- Evd.evar_map * universe_decl
- val default_univ_decl : universe_decl
-end
-
-(************************************************************************)
-(* End of modules from pretyping/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from interp/ *)
-(************************************************************************)
-
-module Tactypes :
-sig
- type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
- type glob_constr_pattern_and_expr = Names.Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
- type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
- type delayed_open_constr = EConstr.constr delayed_open
- type delayed_open_constr_with_bindings = EConstr.constr Misctypes.with_bindings delayed_open
- type intro_pattern = delayed_open_constr Misctypes.intro_pattern_expr Loc.located
- type intro_patterns = delayed_open_constr Misctypes.intro_pattern_expr Loc.located list
- type intro_pattern_naming = Misctypes.intro_pattern_naming_expr Loc.located
- type or_and_intro_pattern = delayed_open_constr Misctypes.or_and_intro_pattern_expr Loc.located
-end
-
-module Genintern :
-sig
- open Genarg
-
- module Store : Store.S
-
- type glob_sign = {
- ltacvars : Names.Id.Set.t;
- genv : Environ.env;
- extra : Store.t;
- }
-
- val empty_glob_sign : Environ.env -> glob_sign
-
- type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
-
-
- val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun
-
- type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb
- val generic_substitute : Genarg.glob_generic_argument subst_fun
-
- type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Names.Id.Map.t -> 'glb -> 'glb
-
- val register_intern0 : ('raw, 'glb, 'top) genarg_type ->
- ('raw, 'glb) intern_fun -> unit
-
- val register_subst0 : ('raw, 'glb, 'top) genarg_type ->
- 'glb subst_fun -> unit
-
- val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type ->
- 'glb ntn_subst_fun -> unit
-
-end
-
-module Stdarg :
-sig
- val loc_of_or_by_notation : ('a -> Loc.t option) -> 'a Misctypes.or_by_notation -> Loc.t option
- val wit_unit : unit Genarg.uniform_genarg_type
- val wit_int : int Genarg.uniform_genarg_type
- val wit_var : (Names.Id.t Loc.located, Names.Id.t Loc.located, Names.Id.t) Genarg.genarg_type
- val wit_bool : bool Genarg.uniform_genarg_type
- val wit_string : string Genarg.uniform_genarg_type
- val wit_pre_ident : string Genarg.uniform_genarg_type
- val wit_global : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type
- val wit_ident : Names.Id.t Genarg.uniform_genarg_type
- val wit_integer : int Genarg.uniform_genarg_type
- val wit_sort_family : (Sorts.family, unit, unit) Genarg.genarg_type
- val wit_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type
- val wit_open_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type
- val wit_intro_pattern : (Constrexpr.constr_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.glob_constr_and_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.intro_pattern) Genarg.genarg_type
- val wit_int_or_var : (int Misctypes.or_var, int Misctypes.or_var, int) Genarg.genarg_type
- val wit_ref : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type
- val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) Genarg.genarg_type
- val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Ltac_pretype.closed_glob_constr) Genarg.genarg_type
- val wit_red_expr :
- ((Constrexpr.constr_expr,Libnames.reference Misctypes.or_by_notation,Constrexpr.constr_expr) Genredexpr.red_expr_gen,
- (Tactypes.glob_constr_and_expr,Names.evaluable_global_reference Misctypes.and_short_name Misctypes.or_var,Tactypes.glob_constr_pattern_and_expr) Genredexpr.red_expr_gen,
- (EConstr.constr,Names.evaluable_global_reference,Pattern.constr_pattern) Genredexpr.red_expr_gen) Genarg.genarg_type
- val wit_quant_hyp : Misctypes.quantified_hypothesis Genarg.uniform_genarg_type
- val wit_bindings :
- (Constrexpr.constr_expr Misctypes.bindings,
- Tactypes.glob_constr_and_expr Misctypes.bindings,
- EConstr.constr Misctypes.bindings Tactypes.delayed_open) Genarg.genarg_type
- val wit_constr_with_bindings :
- (Constrexpr.constr_expr Misctypes.with_bindings,
- Tactypes.glob_constr_and_expr Misctypes.with_bindings,
- EConstr.constr Misctypes.with_bindings Tactypes.delayed_open) Genarg.genarg_type
- val wit_intropattern : (Constrexpr.constr_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.glob_constr_and_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.intro_pattern) Genarg.genarg_type
- val wit_quantified_hypothesis : Misctypes.quantified_hypothesis Genarg.uniform_genarg_type
- val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) Genarg.genarg_type
- val wit_preident : string Genarg.uniform_genarg_type
- val wit_reference : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type
- val wit_open_constr_with_bindings :
- (Constrexpr.constr_expr Misctypes.with_bindings,
- Tactypes.glob_constr_and_expr Misctypes.with_bindings,
- EConstr.constr Misctypes.with_bindings Tactypes.delayed_open) Genarg.genarg_type
-end
-
-module Constrexpr_ops :
-sig
- val mkIdentC : Names.Id.t -> Constrexpr.constr_expr
- val mkAppC : Constrexpr.constr_expr * Constrexpr.constr_expr list -> Constrexpr.constr_expr
- val names_of_local_assums : Constrexpr.local_binder_expr list -> Names.Name.t Loc.located list
- val coerce_reference_to_id : Libnames.reference -> Names.Id.t
- val coerce_to_id : Constrexpr.constr_expr -> Names.Id.t Loc.located
- val constr_loc : Constrexpr.constr_expr -> Loc.t option
- val mkRefC : Libnames.reference -> Constrexpr.constr_expr
- val mkLambdaC : Names.Name.t Loc.located list * Constrexpr.binder_kind * Constrexpr.constr_expr * Constrexpr.constr_expr -> Constrexpr.constr_expr
- val default_binder_kind : Constrexpr.binder_kind
- val mkLetInC : Names.Name.t Loc.located * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr -> Constrexpr.constr_expr
- val mkCProdN : ?loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr
- val replace_vars_constr_expr :
- Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr
-end
-
-module Notation_ops :
-sig
- val glob_constr_of_notation_constr : ?loc:Loc.t -> Notation_term.notation_constr -> Glob_term.glob_constr
- val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
- ('a -> Names.Name.t -> 'a * Names.Name.t) ->
- ('a -> Notation_term.notation_constr -> Glob_term.glob_constr) ->
- 'a -> Notation_term.notation_constr -> Glob_term.glob_constr
-end
-
-module Notation :
-sig
- type cases_pattern_status = bool
- type required_module = Libnames.full_path * string list
- type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> Glob_term.glob_constr
- type 'a prim_token_uninterpreter = Glob_term.glob_constr list * (Glob_term.any_glob_constr -> 'a option) * cases_pattern_status
- type delimiters = string
- type local_scopes = Notation_term.tmp_scope_name option * Notation_term.scope_name list
- type notation_location = (Names.DirPath.t * Names.DirPath.t) * string
- val declare_string_interpreter : Notation_term.scope_name -> required_module ->
- string prim_token_interpreter -> string prim_token_uninterpreter -> unit
- val declare_numeral_interpreter : Notation_term.scope_name -> required_module ->
- Bigint.bigint prim_token_interpreter -> Bigint.bigint prim_token_uninterpreter -> unit
- val interp_notation_as_global_reference : ?loc:Loc.t -> (Globnames.global_reference -> bool) ->
- Constrexpr.notation -> delimiters option -> Globnames.global_reference
- val locate_notation : (Glob_term.glob_constr -> Pp.t) -> Constrexpr.notation ->
- Notation_term.scope_name option -> Pp.t
- val find_delimiters_scope : ?loc:Loc.t -> delimiters -> Notation_term.scope_name
- val pr_scope : (Glob_term.glob_constr -> Pp.t) -> Notation_term.scope_name -> Pp.t
- val pr_scopes : (Glob_term.glob_constr -> Pp.t) -> Pp.t
- val interp_notation : ?loc:Loc.t -> Constrexpr.notation -> local_scopes ->
- Notation_term.interpretation * (notation_location * Notation_term.scope_name option)
- val uninterp_prim_token : Glob_term.glob_constr -> Notation_term.scope_name * Constrexpr.prim_token
-end
-
-module Dumpglob :
-sig
- val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
- val pause : unit -> unit
- val continue : unit -> unit
-end
-
-module Smartlocate :
-sig
- val locate_global_with_alias : ?head:bool -> Libnames.qualid Loc.located -> Globnames.global_reference
- val global_with_alias : ?head:bool -> Libnames.reference -> Globnames.global_reference
- val global_of_extended_global : Globnames.extended_global_reference -> Globnames.global_reference
- val loc_of_smart_reference : Libnames.reference Misctypes.or_by_notation -> Loc.t option
- val smart_global : ?head:bool -> Libnames.reference Misctypes.or_by_notation -> Globnames.global_reference
-end
-
-module Topconstr :
-sig
-
- val replace_vars_constr_expr :
- Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr
- [@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"]
-
-end
-
-module Constrintern :
-sig
-
- open Evd
-
- type ltac_sign = {
- ltac_vars : Names.Id.Set.t;
- ltac_bound : Names.Id.Set.t;
- ltac_extra : Genintern.Store.t;
- }
-
- type var_internalization_data
-
- type var_internalization_type =
- | Inductive of Names.Id.t list * bool
- | Recursive
- | Method
- | Variable
- type internalization_env = var_internalization_data Names.Id.Map.t
-
- val interp_constr_evars : Environ.env -> evar_map ->
- ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.constr
-
- val interp_type_evars : Environ.env -> Evd.evar_map ->
- ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.types
-
- val empty_ltac_sign : ltac_sign
- val intern_gen : Pretyping.typing_constraint -> Environ.env ->
- ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
- Constrexpr.constr_expr -> Glob_term.glob_constr
- val intern_constr_pattern :
- Environ.env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
- Constrexpr.constr_pattern_expr -> Names.Id.t list * Pattern.constr_pattern
- val intern_constr : Environ.env -> Constrexpr.constr_expr -> Glob_term.glob_constr
- val for_grammar : ('a -> 'b) -> 'a -> 'b
- val interp_reference : ltac_sign -> Libnames.reference -> Glob_term.glob_constr
- val interp_constr : Environ.env -> Evd.evar_map -> ?impls:internalization_env ->
- Constrexpr.constr_expr -> Constr.t Evd.in_evar_universe_context
- val interp_open_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.constr
- val locate_reference : Libnames.qualid -> Globnames.global_reference
- val interp_type : Environ.env -> Evd.evar_map -> ?impls:internalization_env ->
- Constrexpr.constr_expr -> Constr.types Evd.in_evar_universe_context
-
- val interp_context_evars :
- ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
- Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list ->
- evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits))
-
- val compute_internalization_data : Environ.env -> var_internalization_type ->
- Constr.types -> Impargs.manual_explicitation list -> var_internalization_data
- val empty_internalization_env : internalization_env
- val global_reference : Names.Id.t -> Globnames.global_reference
-end
-
-module Constrextern :
-sig
- val extern_glob_constr : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr
- val extern_glob_type : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr
- val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr
- val without_symbols : ('a -> 'b) -> 'a -> 'b
- val print_universes : bool ref
- val extern_type : bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr
- val with_universes : ('a -> 'b) -> 'a -> 'b
- val set_extern_reference :
- (?loc:Loc.t -> Names.Id.Set.t -> Globnames.global_reference -> Libnames.reference) -> unit
-end
-
-module Declare :
-sig
- type internal_flag =
- | UserAutomaticRequest
- | InternalTacticRequest
- | UserIndividualRequest
-
- type constant_declaration = Safe_typing.private_constants Entries.constant_entry * Decl_kinds.logical_kind
-
- type section_variable_entry =
- | SectionLocalDef of Safe_typing.private_constants Entries.definition_entry
- | SectionLocalAssum of Constr.types Univ.in_universe_context_set * Decl_kinds.polymorphic * bool
-
- type variable_declaration = Names.DirPath.t * section_variable_entry * Decl_kinds.logical_kind
-
- val declare_constant :
- ?internal:internal_flag -> ?local:bool -> Names.Id.t -> ?export_seff:bool -> constant_declaration -> Names.Constant.t
-
- val declare_universe_context : Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
-
- val declare_definition :
- ?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind ->
- ?local:bool -> Names.Id.t -> ?types:Constr.t ->
- Constr.t Entries.in_constant_universes_entry -> Names.Constant.t
- val definition_entry : ?fix_exn:Future.fix_exn ->
- ?opaque:bool -> ?inline:bool -> ?types:Constr.types ->
- ?univs:Entries.constant_universes_entry ->
- ?eff:Safe_typing.private_constants -> Constr.t -> Safe_typing.private_constants Entries.definition_entry
- val definition_message : Names.Id.t -> unit
- val declare_variable : Names.Id.t -> variable_declaration -> Libnames.object_name
-end
-
-(************************************************************************)
-(* End of modules from interp/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from proofs/ *)
-(************************************************************************)
-
-module Miscprint :
-sig
- val pr_or_and_intro_pattern :
- ('a -> Pp.t) -> 'a Misctypes.or_and_intro_pattern_expr -> Pp.t
- val pr_intro_pattern_naming : Misctypes.intro_pattern_naming_expr -> Pp.t
- val pr_intro_pattern :
- ('a -> Pp.t) -> 'a Misctypes.intro_pattern_expr Loc.located -> Pp.t
- val pr_bindings :
- ('a -> Pp.t) ->
- ('a -> Pp.t) -> 'a Misctypes.bindings -> Pp.t
- val pr_bindings_no_with :
- ('a -> Pp.t) ->
- ('a -> Pp.t) -> 'a Misctypes.bindings -> Pp.t
- val pr_with_bindings :
- ('a -> Pp.t) ->
- ('a -> Pp.t) -> 'a * 'a Misctypes.bindings -> Pp.t
-end
-
-(* All items in the Goal modules are deprecated. *)
-module Goal :
-sig
- type goal = Evar.t
-
- val pr_goal : goal -> Pp.t
-
- module V82 :
- sig
- val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma
-
- val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val
-
- val env : Evd.evar_map -> goal -> Environ.env
-
- val concl : Evd.evar_map -> goal -> EConstr.constr
-
- val mk_goal : Evd.evar_map ->
- Environ.named_context_val ->
- EConstr.constr ->
- Evd.Store.t ->
- goal * EConstr.constr * Evd.evar_map
-
- val extra : Evd.evar_map -> goal -> Evd.Store.t
-
- val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
-
- val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
-
- val hyps : Evd.evar_map -> goal -> Environ.named_context_val
-
- val abstract_type : Evd.evar_map -> goal -> EConstr.types
- end
-end
-
-module Evar_refiner :
-sig
- type glob_constr_ltac_closure = Ltac_pretype.ltac_var_map * Glob_term.glob_constr
-
- val w_refine : Evar.t * Evd.evar_info ->
- glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map
-end
-
-
-module Proof_type :
-sig
- type prim_rule = Refine of Constr.t
-
- type tactic = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-end
-
-module Logic :
-sig
- type refiner_error =
- | BadType of Constr.t * Constr.t * Constr.t
- | UnresolvedBindings of Names.Name.t list
- | CannotApply of Constr.t * Constr.t
- | NotWellTyped of Constr.t
- | NonLinearProof of Constr.t
- | MetaInType of EConstr.constr
- | IntroNeedsProduct
- | DoesNotOccurIn of Constr.t * Names.Id.t
- | NoSuchHyp of Names.Id.t
- exception RefinerError of Environ.env * Evd.evar_map * refiner_error
- val catchable_exception : exn -> bool
-end
-
-module Refine :
-sig
- val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic
- val solve_constraints : unit Proofview.tactic
-end
-
-module Proof :
-sig
- type t
- type proof = t
- [@@ocaml.deprecated "please use [Proof.t]"]
-
- type 'a focus_kind
- val proof : t ->
- Goal.goal list * (Goal.goal list * Goal.goal list) list *
- Goal.goal list * Goal.goal list * Evd.evar_map
-
- val run_tactic : Environ.env ->
- unit Proofview.tactic -> t -> t * (bool * Proofview_monad.Info.tree)
- val unshelve : t -> t
- val maximal_unfocus : 'a focus_kind -> t -> t
- val pr_proof : t -> Pp.t
-
- module V82 :
- sig
- val grab_evars : t -> t
-
- val subgoals : t -> Goal.goal list Evd.sigma
- [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
-
- end
-end
-
-module Proof_bullet :
-sig
- val get_default_goal_selector : unit -> Vernacexpr.goal_selector
-end
-
-module Proof_global :
-sig
-
- type t
- type state = t
- [@@ocaml.deprecated "please use [Proof_global.t]"]
-
- type proof_mode = {
- name : string;
- set : unit -> unit ;
- reset : unit -> unit
- }
- type proof_object = {
- id : Names.Id.t;
- entries : Safe_typing.private_constants Entries.definition_entry list;
- persistence : Decl_kinds.goal_kind;
- universes: UState.t;
- }
-
- type proof_ending =
- | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
- UState.t
- | Proved of Vernacexpr.opacity_flag *
- Vernacexpr.lident option *
- proof_object
-
- type proof_terminator
- type lemma_possible_guards
- type closed_proof = proof_object * proof_terminator
-
- val make_terminator : (proof_ending -> unit) -> proof_terminator
- val start_dependent_proof :
- Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
- Proofview.telescope -> proof_terminator -> unit
- val with_current_proof :
- (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
- val simple_with_current_proof :
- (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
- val compact_the_proof : unit -> unit
- val register_proof_mode : proof_mode -> unit
-
- exception NoCurrentProof
- val give_me_the_proof : unit -> Proof.t
- (** @raise NoCurrentProof when outside proof mode. *)
-
- val discard_all : unit -> unit
- val discard_current : unit -> unit
- val get_current_proof_name : unit -> Names.Id.t
-end
-
-module Redexpr :
-sig
- type red_expr =
- (EConstr.constr, Names.evaluable_global_reference, Pattern.constr_pattern) Genredexpr.red_expr_gen
- val reduction_of_red_expr :
- Environ.env -> red_expr -> Reductionops.e_reduction_function * Constr.cast_kind
- val declare_reduction : string -> Reductionops.reduction_function -> unit
-end
-
-module Refiner :
-sig
- val project : 'a Evd.sigma -> Evd.evar_map
-
- val unpackage : 'a Evd.sigma -> Evd.evar_map ref * 'a
-
- val repackage : Evd.evar_map ref -> 'a -> 'a Evd.sigma
-
- val tclSHOWHYPS : Proof_type.tactic -> Proof_type.tactic
- exception FailError of int * Pp.t Lazy.t
-
- val tclEVARS : Evd.evar_map -> Proof_type.tactic
- val tclMAP : ('a -> Proof_type.tactic) -> 'a list -> Proof_type.tactic
- val tclREPEAT : Proof_type.tactic -> Proof_type.tactic
- val tclORELSE : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
- val tclFAIL : int -> Pp.t -> Proof_type.tactic
- val tclIDTAC : Proof_type.tactic
- val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
- val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic
- val tclTRY : Proof_type.tactic -> Proof_type.tactic
- val tclAT_LEAST_ONCE : Proof_type.tactic -> Proof_type.tactic
-end
-
-module Tacmach :
-sig
-
- type tactic = Proof_type.tactic
-
- type 'a sigma = 'a Evd.sigma
- [@@ocaml.deprecated "alias of API.Evd.sigma"]
-
- val re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma
-
- val pf_reduction_of_red_expr : Goal.goal Evd.sigma -> Redexpr.red_expr -> EConstr.constr -> Evd.evar_map * EConstr.constr
-
- val pf_unsafe_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types
-
- val pf_get_new_id : Names.Id.t -> Goal.goal Evd.sigma -> Names.Id.t
-
- val pf_env : Goal.goal Evd.sigma -> Environ.env
-
- val pf_concl : Goal.goal Evd.sigma -> EConstr.types
-
- val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Goal.goal Evd.sigma -> 'a
-
- val pf_get_hyp : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.named_declaration
- val pf_get_hyp_typ : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.types
- val project : Goal.goal Evd.sigma -> Evd.evar_map
- val refine : EConstr.constr -> Proof_type.tactic
- val refine_no_check : EConstr.constr -> Proof_type.tactic
- val pf_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Evd.evar_map * EConstr.types
-
- val pf_hyps : Goal.goal Evd.sigma -> EConstr.named_context
-
- val pf_ids_of_hyps : Goal.goal Evd.sigma -> Names.Id.t list
-
- val pf_reduce_to_atomic_ind : Goal.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types
-
- val pf_reduce_to_quantified_ind : Goal.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types
-
- val pf_eapply : (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) ->
- Evar.t Evd.sigma -> 'a -> Evar.t Evd.sigma * 'b
-
- val pf_unfoldn : (Locus.occurrences * Names.evaluable_global_reference) list
- -> Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
-
- val pf_reduce : (Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr) -> Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
-
- val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
-
- val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list
-
- val pr_gls : Goal.goal Evd.sigma -> Pp.t
-
- val pf_nf_betaiota : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
-
- val pf_last_hyp : Goal.goal Evd.sigma -> EConstr.named_declaration
-
- val pf_nth_hyp_id : Goal.goal Evd.sigma -> int -> Names.Id.t
-
- val sig_it : 'a Evd.sigma -> 'a
-
- module New :
- sig
- val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
- val project : 'a Proofview.Goal.t -> Evd.evar_map
- val pf_unsafe_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types
- val of_old : (Goal.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
-
- val pf_env : 'a Proofview.Goal.t -> Environ.env
- val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.Id.t list
- val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Names.Id.Set.t
- val pf_concl : 'a Proofview.Goal.t -> EConstr.types
- val pf_get_new_id : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t
- val pf_get_hyp : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.named_declaration
- val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types
- val pf_get_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types
- val pf_global : Names.Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference
- val pf_hyps_types : 'a Proofview.Goal.t -> (Names.Id.t * EConstr.types) list
- end
-end
-
-module Pfedit :
-sig
- val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
- val refine_by_tactic : Environ.env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
- Constr.t * Evd.evar_map
- val declare_implicit_tactic : unit Proofview.tactic -> unit
- val clear_implicit_tactic : unit -> unit
- val by : unit Proofview.tactic -> bool
- val solve : ?with_end_tac:unit Proofview.tactic ->
- Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
- Proof.t -> Proof.t * bool
- val cook_proof :
- unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * UState.t * Decl_kinds.goal_kind))
-
- val get_current_context : unit -> Evd.evar_map * Environ.env
- val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types
-end
-
-module Clenv :
-sig
-
- type hole = {
- hole_evar : EConstr.constr;
- hole_type : EConstr.types;
- hole_deps : bool;
- hole_name : Names.Name.t;
- }
-
- type clause = {
- cl_holes : hole list;
- cl_concl : EConstr.types;
- }
-
- val make_evar_clause : Environ.env -> Evd.evar_map -> ?len:int -> EConstr.types ->
- (Evd.evar_map * clause)
- val solve_evar_clause : Environ.env -> Evd.evar_map -> bool -> clause -> EConstr.constr Misctypes.bindings ->
- Evd.evar_map
- type clausenv
- val pr_clenv : clausenv -> Pp.t
-end
-
-(************************************************************************)
-(* End of modules from proofs/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from parsing/ *)
-(************************************************************************)
-
-module Pcoq :
-sig
-
- open Loc
- open Names
- open Extend
- open Vernacexpr
- open Genarg
- open Constrexpr
- open Libnames
- open Misctypes
- open Genredexpr
-
- module Gram : sig
- include Grammar.S with type te = Tok.t
-
- type 'a entry = 'a Entry.e
- type internal_entry = Tok.t Gramext.g_entry
- type symbol = Tok.t Gramext.g_symbol
- type action = Gramext.g_action
- type production_rule = symbol list * action
- type single_extend_statment =
- string option * Gramext.g_assoc option * production_rule list
- type extend_statment =
- Gramext.position option * single_extend_statment list
-
- type coq_parsable
-
- val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
- val action : 'a -> action
- val entry_create : string -> 'a entry
- val entry_parse : 'a entry -> coq_parsable -> 'a
- val entry_print : Format.formatter -> 'a entry -> unit
- val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
-
- (* Apparently not used *)
- val srules' : production_rule list -> symbol
- val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
-
- end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
-
- val parse_string : 'a Gram.entry -> string -> 'a
- val eoi_entry : 'a Gram.entry -> 'a Gram.entry
- val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
-
- type gram_universe
-
- val uprim : gram_universe
- val uconstr : gram_universe
- val utactic : gram_universe
- val uvernac : gram_universe
-
- val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
-
- val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
-
- val create_generic_entry : gram_universe -> string ->
- ('a, rlevel) abstract_argument_type -> 'a Gram.entry
-
- module Prim :
- sig
- open Names
- open Libnames
- val preident : string Gram.entry
- val ident : Id.t Gram.entry
- val name : Name.t located Gram.entry
- val identref : Id.t located Gram.entry
- val pattern_ident : Id.t Gram.entry
- val pattern_identref : Id.t located Gram.entry
- val base_ident : Id.t Gram.entry
- val natural : int Gram.entry
- val bigint : Constrexpr.raw_natural_number Gram.entry
- val integer : int Gram.entry
- val string : string Gram.entry
- val lstring : string located Gram.entry
- val qualid : qualid located Gram.entry
- val fullyqualid : Id.t list located Gram.entry
- val reference : reference Gram.entry
- val by_notation : (string * string option) Loc.located Gram.entry
- val smart_global : reference or_by_notation Gram.entry
- val dirpath : DirPath.t Gram.entry
- val ne_string : string Gram.entry
- val ne_lstring : string located Gram.entry
- val var : Id.t located Gram.entry
- end
-
- module Constr :
- sig
- val constr : constr_expr Gram.entry
- val constr_eoi : constr_expr Gram.entry
- val lconstr : constr_expr Gram.entry
- val binder_constr : constr_expr Gram.entry
- val operconstr : constr_expr Gram.entry
- val ident : Id.t Gram.entry
- val global : reference Gram.entry
- val universe_level : glob_level Gram.entry
- val sort : glob_sort Gram.entry
- val sort_family : Sorts.family Gram.entry
- val pattern : cases_pattern_expr Gram.entry
- val constr_pattern : constr_expr Gram.entry
- val lconstr_pattern : constr_expr Gram.entry
- val closed_binder : local_binder_expr list Gram.entry
- val binder : local_binder_expr list Gram.entry (* closed_binder or variable *)
- val binders : local_binder_expr list Gram.entry (* list of binder *)
- val open_binders : local_binder_expr list Gram.entry
- val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry
- val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry
- val record_declaration : constr_expr Gram.entry
- val appl_arg : (constr_expr * explicitation located option) Gram.entry
- end
-
- module Vernac_ :
- sig
- val gallina : vernac_expr Gram.entry
- val gallina_ext : vernac_expr Gram.entry
- val command : vernac_expr Gram.entry
- val syntax : vernac_expr Gram.entry
- val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
- val noedit_mode : vernac_expr Gram.entry
- val command_entry : vernac_expr Gram.entry
- val red_expr : raw_red_expr Gram.entry
- val hint_info : Vernacexpr.hint_info_expr Gram.entry
- end
-
- val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
-
- val get_command_entry : unit -> vernac_expr Gram.entry
- val set_command_entry : vernac_expr Gram.entry -> unit
-
- type gram_reinit = gram_assoc * gram_position
- val grammar_extend : 'a Gram.entry -> gram_reinit option ->
- 'a Extend.extend_statment -> unit
-
- module GramState : Store.S
-
- type 'a grammar_command
-
- type extend_rule =
- | ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule
-
- type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
-
- val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command
-
- val extend_grammar_command : 'a grammar_command -> 'a -> unit
- val recover_grammar_command : 'a grammar_command -> 'a list
- val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
-
- val to_coqloc : Ploc.t -> Loc.t
- val (!@) : Ploc.t -> Loc.t
-
-end
-
-module Egramml :
-sig
- open Vernacexpr
-
- type 's grammar_prod_item =
- | GramTerminal of string
- | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option *
- ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
-
- val extend_vernac_command_grammar :
- extend_name -> vernac_expr Pcoq.Gram.entry option ->
- vernac_expr grammar_prod_item list -> unit
-
- val make_rule :
- (Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
- 'a grammar_prod_item list -> 'a Extend.production_rule
-
-end
-
-module G_vernac :
-sig
-
- val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry
- val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry
- val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry
-
-end
-
-module G_proofs :
-sig
-
- val hint : Vernacexpr.hints_expr Pcoq.Gram.entry
-
-end
-
-(************************************************************************)
-(* End of modules from parsing/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from printing/ *)
-(************************************************************************)
-
-module Genprint :
-sig
- type 'a with_level =
- { default_already_surrounded : Notation_term.tolerability;
- default_ensure_surrounded : Notation_term.tolerability;
- printer : 'a }
- type printer_result =
-| PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
- type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
- type top_printer_result =
- | TopPrinterBasic of (unit -> Pp.t)
- | TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
- | TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
- type 'a printer = 'a -> printer_result
- type 'a top_printer = 'a -> top_printer_result
- val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
- 'raw printer -> 'glb printer -> 'top top_printer -> unit
- val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
- 'raw printer -> unit
- val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit
- val generic_top_print : Genarg.tlevel Genarg.generic_argument top_printer
- val generic_val_print : Geninterp.Val.t top_printer
-end
-
-module Pputils :
-sig
- val pr_with_occurrences : ('a -> Pp.t) -> (string -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t
- val pr_red_expr :
- ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
- (string -> Pp.t) ->
- ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t
- val pr_raw_generic : Environ.env -> Genarg.rlevel Genarg.generic_argument -> Pp.t
- val pr_glb_generic : Environ.env -> Genarg.glevel Genarg.generic_argument -> Pp.t
- val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t
- val pr_or_by_notation : ('a -> Pp.t) -> 'a Misctypes.or_by_notation -> Pp.t
-end
-
-module Ppconstr :
-sig
- val pr_name : Names.Name.t -> Pp.t
- [@@ocaml.deprecated "alias of API.Names.Name.print"]
-
- val lsimpleconstr : Notation_term.tolerability
- val ltop : Notation_term.tolerability
- val pr_id : Names.Id.t -> Pp.t
- val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t
- val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
- val pr_lident : Names.Id.t Loc.located -> Pp.t
- val pr_lname : Names.Name.t Loc.located -> Pp.t
- val prec_less : int -> int * Notation_term.parenRelation -> bool
- val pr_constr_expr : Constrexpr.constr_expr -> Pp.t
- val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.t
- val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t
- val pr_lconstr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t
- val pr_binders : Constrexpr.local_binder_expr list -> Pp.t
- val pr_glob_sort : Misctypes.glob_sort -> Pp.t
-end
-
-module Printer :
-sig
- val pr_named_context : Environ.env -> Evd.evar_map -> Context.Named.t -> Pp.t
- val pr_rel_context : Environ.env -> Evd.evar_map -> Context.Rel.t -> Pp.t
- val pr_goal : Goal.goal Evd.sigma -> Pp.t
-
- val pr_constr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t
- val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t
-
- val pr_constr : Constr.t -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-
- val pr_lconstr : Constr.t -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-
- val pr_econstr : EConstr.constr -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-
- val pr_glob_constr : Glob_term.glob_constr -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-
- val pr_constr_pattern : Pattern.constr_pattern -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-
- val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
- val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
- val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t
- val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
- val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
- val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
- val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
- val pr_lglob_constr : Glob_term.glob_constr -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
- val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
- val pr_leconstr : EConstr.constr -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-
- val pr_global : Globnames.global_reference -> Pp.t
- val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-
- val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
-
- val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
- val pr_closed_glob_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Ltac_pretype.closed_glob_constr -> Pp.t
- val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t
- val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t
- val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t
- val pr_ltype : Constr.types -> Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
- val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t
- [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-
- val pr_idpred : Names.Id.Pred.t -> Pp.t
- val pr_cpred : Names.Cpred.t -> Pp.t
- val pr_transparent_state : Names.transparent_state -> Pp.t
-end
-
-module Prettyp :
-sig
- type 'a locatable_info = {
- locate : Libnames.qualid -> 'a option;
- locate_all : Libnames.qualid -> 'a list;
- shortest_qualid : 'a -> Libnames.qualid;
- name : 'a -> Pp.t;
- print : 'a -> Pp.t;
- about : 'a -> Pp.t;
- }
-
- val register_locatable : string -> 'a locatable_info -> unit
- val print_located_other : string -> Libnames.reference -> Pp.t
-end
-
-(************************************************************************)
-(* End of modules from printing/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from tactics/ *)
-(************************************************************************)
-
-module Tacticals :
-sig
- open Proof_type
-
- val tclORELSE : tactic -> tactic -> tactic
- val tclDO : int -> tactic -> tactic
- val tclIDTAC : tactic
- val tclFAIL : int -> Pp.t -> tactic
- val tclTHEN : tactic -> tactic -> tactic
- val tclTHENLIST : tactic list -> tactic
- val pf_constr_of_global :
- Globnames.global_reference -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic
- val tclMAP : ('a -> tactic) -> 'a list -> tactic
- val tclTRY : tactic -> tactic
- val tclCOMPLETE : tactic -> tactic
- val tclTHENS : tactic -> tactic list -> tactic
- val tclFIRST : tactic list -> tactic
- val tclTHENFIRST : tactic -> tactic -> tactic
- val tclTHENLAST : tactic -> tactic -> tactic
- val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
- val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
- val tclSOLVE : tactic list -> tactic
-
- val onClause : (Names.Id.t option -> tactic) -> Locus.clause -> tactic
- val onAllHypsAndConcl : (Names.Id.t option -> tactic) -> tactic
- val onLastHypId : (Names.Id.t -> tactic) -> tactic
- val onNthHypId : int -> (Names.Id.t -> tactic) -> tactic
- val onNLastHypsId : int -> (Names.Id.t list -> tactic) -> tactic
-
- val tclTHENSEQ : tactic list -> tactic
- [@@ocaml.deprecated "alias of API.Tacticals.tclTHENLIST"]
-
- val nLastDecls : int -> Goal.goal Evd.sigma -> EConstr.named_context
-
- val tclTHEN_i : tactic -> (int -> tactic) -> tactic
-
- val tclPROGRESS : tactic -> tactic
-
- val elimination_sort_of_goal : Goal.goal Evd.sigma -> Sorts.family
-
- module New :
- sig
- open Proofview
- val tclORELSE0 : unit tactic -> unit tactic -> unit tactic
- val tclFAIL : int -> Pp.t -> 'a tactic
- val pf_constr_of_global : Globnames.global_reference -> EConstr.constr tactic
- val tclTHEN : unit tactic -> unit tactic -> unit tactic
- val tclTHENS : unit tactic -> unit tactic list -> unit tactic
- val tclFIRST : unit tactic list -> unit tactic
- val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic
- val tclORELSE : unit tactic -> unit tactic -> unit tactic
- val tclREPEAT : unit tactic -> unit tactic
- val tclTRY : unit tactic -> unit tactic
- val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic
- val tclPROGRESS : unit Proofview.tactic -> unit Proofview.tactic
- val tclTHENS3PARTS : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic
- val tclDO : int -> unit tactic -> unit tactic
- val tclTIMEOUT : int -> unit tactic -> unit tactic
- val tclTIME : string option -> 'a tactic -> 'a tactic
- val tclOR : unit tactic -> unit tactic -> unit tactic
- val tclONCE : unit tactic -> unit tactic
- val tclEXACTLY_ONCE : unit tactic -> unit tactic
- val tclIFCATCH :
- unit tactic ->
- (unit -> unit tactic) ->
- (unit -> unit tactic) -> unit tactic
- val tclSOLVE : unit tactic list -> unit tactic
- val tclCOMPLETE : 'a tactic -> 'a tactic
- val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic
- val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
- val tclDELAYEDWITHHOLES : bool -> 'a Tactypes.delayed_open -> ('a -> unit tactic) -> unit tactic
- val tclTHENLIST : unit tactic list -> unit tactic
- val tclTHENLAST : unit tactic -> unit tactic -> unit tactic
- val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic
- val tclIDTAC : unit tactic
- val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic
- val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic
- end
-end
-
-module Hipattern :
-sig
- exception NoEquationFound
- type 'a matching_function = Evd.evar_map -> EConstr.constr -> 'a option
- type testing_function = Evd.evar_map -> EConstr.constr -> bool
- val is_disjunction : ?strict:bool -> ?onlybinary:bool -> testing_function
- val match_with_disjunction : ?strict:bool -> ?onlybinary:bool -> (EConstr.constr * EConstr.constr list) matching_function
- val match_with_equality_type : (EConstr.constr * EConstr.constr list) matching_function
- val is_empty_type : testing_function
- val is_unit_type : testing_function
- val is_unit_or_eq_type : testing_function
- val is_conjunction : ?strict:bool -> ?onlybinary:bool -> testing_function
- val match_with_conjunction : ?strict:bool -> ?onlybinary:bool -> (EConstr.constr * EConstr.constr list) matching_function
- val match_with_imp_term : (EConstr.constr * EConstr.constr) matching_function
- val match_with_forall_term : (Names.Name.t * EConstr.constr * EConstr.constr) matching_function
- val match_with_nodep_ind : (EConstr.constr * EConstr.constr list * int) matching_function
- val match_with_sigma_type : (EConstr.constr * EConstr.constr list) matching_function
-end
-
-module Ind_tables :
-sig
- type individual
- type 'a scheme_kind
-
- val check_scheme : 'a scheme_kind -> Names.inductive -> bool
- val find_scheme : ?mode:Declare.internal_flag -> 'a scheme_kind -> Names.inductive -> Names.Constant.t * Safe_typing.private_constants
- val pr_scheme_kind : 'a scheme_kind -> Pp.t
-end
-
-module Elimschemes :
-sig
- val case_scheme_kind_from_prop : Ind_tables.individual Ind_tables.scheme_kind
- val case_dep_scheme_kind_from_type_in_prop : Ind_tables.individual Ind_tables.scheme_kind
- val case_scheme_kind_from_type : Ind_tables.individual Ind_tables.scheme_kind
- val case_dep_scheme_kind_from_type : Ind_tables.individual Ind_tables.scheme_kind
- val case_dep_scheme_kind_from_prop : Ind_tables.individual Ind_tables.scheme_kind
-end
-
-module Tactics :
-sig
- open Proofview
-
- type change_arg = Ltac_pretype.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr
- type tactic_reduction = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
-
- type elim_scheme =
- {
- elimc: EConstr.constr Misctypes.with_bindings option;
- elimt: EConstr.types;
- indref: Globnames.global_reference option;
- params: EConstr.rel_context;
- nparams: int;
- predicates: EConstr.rel_context;
- npredicates: int;
- branches: EConstr.rel_context;
- nbranches: int;
- args: EConstr.rel_context;
- nargs: int;
- indarg: EConstr.rel_declaration option;
- concl: EConstr.types;
- indarg_in_concl: bool;
- farg_in_concl: bool;
- }
-
- val unify : ?state:Names.transparent_state -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic
- val intro_then : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
- val reflexivity : unit tactic
- val change_concl : EConstr.constr -> unit tactic
- val apply : EConstr.constr -> unit tactic
- val normalise_vm_in_concl : unit tactic
- val assert_before : Names.Name.t -> EConstr.types -> unit tactic
- val exact_check : EConstr.constr -> unit tactic
- val simplest_elim : EConstr.constr -> unit tactic
- val introf : unit tactic
- val cut : EConstr.types -> unit tactic
- val convert_concl : ?check:bool -> EConstr.types -> Constr.cast_kind -> unit tactic
- val intro_using : Names.Id.t -> unit tactic
- val intro : unit tactic
- val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t
- val is_quantified_hypothesis : Names.Id.t -> 'a Goal.t -> bool
- val tclABSTRACT : ?opaque:bool -> Names.Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
- val intro_patterns : bool -> Tactypes.intro_patterns -> unit Proofview.tactic
- val apply_with_delayed_bindings_gen :
- Misctypes.advanced_flag -> Misctypes.evars_flag -> (Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings Loc.located) list -> unit Proofview.tactic
- val apply_delayed_in :
- Misctypes.advanced_flag -> Misctypes.evars_flag -> Names.Id.t ->
- (Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings Loc.located) list ->
- Tactypes.intro_pattern option -> unit Proofview.tactic
- val elim :
- Misctypes.evars_flag -> Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> EConstr.constr Misctypes.with_bindings option -> unit Proofview.tactic
- val general_case_analysis : Misctypes.evars_flag -> Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
- val mutual_fix :
- Names.Id.t -> int -> (Names.Id.t * int * EConstr.constr) list -> int -> unit Proofview.tactic
- val mutual_cofix : Names.Id.t -> (Names.Id.t * EConstr.constr) list -> int -> unit Proofview.tactic
- val forward : bool -> unit Proofview.tactic option option ->
- Tactypes.intro_pattern option -> EConstr.constr -> unit Proofview.tactic
- val generalize_gen : (EConstr.constr Locus.with_occurrences * Names.Name.t) list -> unit Proofview.tactic
- val letin_tac : (bool * Tactypes.intro_pattern_naming) option ->
- Names.Name.t -> EConstr.constr -> EConstr.types option -> Locus.clause -> unit Proofview.tactic
- val letin_pat_tac : Misctypes.evars_flag ->
- (bool * Tactypes.intro_pattern_naming) option ->
- Names.Name.t ->
- Evd.evar_map * EConstr.constr ->
- Locus.clause -> unit Proofview.tactic
- val induction_destruct : Misctypes.rec_flag -> Misctypes.evars_flag ->
- (Tactypes.delayed_open_constr_with_bindings Misctypes.destruction_arg
- * (Tactypes.intro_pattern_naming option * Tactypes.or_and_intro_pattern option)
- * Locus.clause option) list *
- EConstr.constr Misctypes.with_bindings option -> unit Proofview.tactic
- val reduce : Redexpr.red_expr -> Locus.clause -> unit Proofview.tactic
- val change : Pattern.constr_pattern option -> change_arg -> Locus.clause -> unit Proofview.tactic
- val intros_reflexivity : unit Proofview.tactic
- val exact_no_check : EConstr.constr -> unit Proofview.tactic
- val assumption : unit Proofview.tactic
- val intros_transitivity : EConstr.constr option -> unit Proofview.tactic
- val vm_cast_no_check : EConstr.constr -> unit Proofview.tactic
- val native_cast_no_check : EConstr.constr -> unit Proofview.tactic
- val case_type : EConstr.types -> unit Proofview.tactic
- val elim_type : EConstr.types -> unit Proofview.tactic
- val cut_and_apply : EConstr.constr -> unit Proofview.tactic
- val left_with_bindings : Misctypes.evars_flag -> EConstr.constr Misctypes.bindings -> unit Proofview.tactic
- val right_with_bindings : Misctypes.evars_flag -> EConstr.constr Misctypes.bindings -> unit Proofview.tactic
- val any_constructor : Misctypes.evars_flag -> unit Proofview.tactic option -> unit Proofview.tactic
- val constructor_tac : Misctypes.evars_flag -> int option -> int ->
- EConstr.constr Misctypes.bindings -> unit Proofview.tactic
- val specialize : EConstr.constr Misctypes.with_bindings -> Tactypes.intro_pattern option -> unit Proofview.tactic
- val intros_symmetry : Locus.clause -> unit Proofview.tactic
- val split_with_bindings : Misctypes.evars_flag -> EConstr.constr Misctypes.bindings list -> unit Proofview.tactic
- val intros_until : Misctypes.quantified_hypothesis -> unit Proofview.tactic
- val intro_move : Names.Id.t option -> Names.Id.t Misctypes.move_location -> unit Proofview.tactic
- val move_hyp : Names.Id.t -> Names.Id.t Misctypes.move_location -> unit Proofview.tactic
- val rename_hyp : (Names.Id.t * Names.Id.t) list -> unit Proofview.tactic
- val revert : Names.Id.t list -> unit Proofview.tactic
- val simple_induct : Misctypes.quantified_hypothesis -> unit Proofview.tactic
- val simple_destruct : Misctypes.quantified_hypothesis -> unit Proofview.tactic
- val fix : Names.Id.t option -> int -> unit Proofview.tactic
- val cofix : Names.Id.t option -> unit Proofview.tactic
- val keep : Names.Id.t list -> unit Proofview.tactic
- val clear : Names.Id.t list -> unit Proofview.tactic
- val clear_body : Names.Id.t list -> unit Proofview.tactic
- val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> EConstr.constr -> unit Proofview.tactic
- val force_destruction_arg : Misctypes.evars_flag -> Environ.env -> Evd.evar_map ->
- Tactypes.delayed_open_constr_with_bindings Misctypes.destruction_arg ->
- Evd.evar_map * EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg
- val apply_with_bindings : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
- val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Names.Id.t -> unit Proofview.tactic
- val specialize_eqs : Names.Id.t -> unit Proofview.tactic
- val generalize : EConstr.constr list -> unit Proofview.tactic
- val simplest_case : EConstr.constr -> unit Proofview.tactic
- val introduction : ?check:bool -> Names.Id.t -> unit Proofview.tactic
- val convert_concl_no_check : EConstr.types -> Constr.cast_kind -> unit Proofview.tactic
- val reduct_in_concl : tactic_reduction * Constr.cast_kind -> unit Proofview.tactic
- val reduct_in_hyp : ?check:bool -> tactic_reduction -> Locus.hyp_location -> unit Proofview.tactic
- val convert_hyp_no_check : EConstr.named_declaration -> unit Proofview.tactic
- val reflexivity_red : bool -> unit Proofview.tactic
- val symmetry_red : bool -> unit Proofview.tactic
- val eapply : EConstr.constr -> unit Proofview.tactic
- val transitivity_red : bool -> EConstr.constr option -> unit Proofview.tactic
- val assert_after_replacing : Names.Id.t -> EConstr.types -> unit Proofview.tactic
- val intros : unit Proofview.tactic
- val setoid_reflexivity : unit Proofview.tactic Hook.t
- val setoid_symmetry : unit Proofview.tactic Hook.t
- val setoid_symmetry_in : (Names.Id.t -> unit Proofview.tactic) Hook.t
- val setoid_transitivity : (EConstr.constr option -> unit Proofview.tactic) Hook.t
- val unfold_in_concl :
- (Locus.occurrences * Names.evaluable_global_reference) list -> unit Proofview.tactic
- val intros_using : Names.Id.t list -> unit Proofview.tactic
- val simpl_in_concl : unit Proofview.tactic
- val reduct_option : ?check:bool -> tactic_reduction * Constr.cast_kind -> Locus.goal_location -> unit Proofview.tactic
- val simplest_split : unit Proofview.tactic
- val unfold_in_hyp :
- (Locus.occurrences * Names.evaluable_global_reference) list -> Locus.hyp_location -> unit Proofview.tactic
- val split : EConstr.constr Misctypes.bindings -> unit Proofview.tactic
- val red_in_concl : unit Proofview.tactic
- val change_in_concl : (Locus.occurrences * Pattern.constr_pattern) option -> change_arg -> unit Proofview.tactic
- val eapply_with_bindings : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
- val assert_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic ->
- unit Proofview.tactic
- val intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic
- val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic
- val pattern_option : (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic
- val compute_elim_sig : Evd.evar_map -> ?elimc:EConstr.constr Misctypes.with_bindings -> EConstr.types -> elim_scheme
- val try_intros_until :
- (Names.Id.t -> unit Proofview.tactic) -> Misctypes.quantified_hypothesis -> unit Proofview.tactic
- val cache_term_by_tactic_then :
- opaque:bool -> ?goal_type:(EConstr.constr option) -> Names.Id.t ->
- Decl_kinds.goal_kind -> unit Proofview.tactic -> (EConstr.constr -> EConstr.constr list -> unit Proofview.tactic) -> unit Proofview.tactic
- val apply_type : EConstr.constr -> EConstr.constr list -> unit Proofview.tactic
- val hnf_in_concl : unit Proofview.tactic
- val intro_mustbe_force : Names.Id.t -> unit Proofview.tactic
-
- module New :
- sig
- val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
- val reduce_after_refine : unit Proofview.tactic
- end
- module Simple :
- sig
- val intro : Names.Id.t -> unit Proofview.tactic
- val apply : EConstr.constr -> unit Proofview.tactic
- val case : EConstr.constr -> unit Proofview.tactic
- end
-end
-
-module Elim :
-sig
- val h_decompose : Names.inductive list -> EConstr.constr -> unit Proofview.tactic
- val h_double_induction : Misctypes.quantified_hypothesis -> Misctypes.quantified_hypothesis-> unit Proofview.tactic
- val h_decompose_or : EConstr.constr -> unit Proofview.tactic
- val h_decompose_and : EConstr.constr -> unit Proofview.tactic
-end
-
-module Equality :
-sig
- type orientation = bool
- type freeze_evars_flag = bool
- type dep_proof_flag = bool
- type conditions =
- | Naive
- | FirstSolved
- | AllMatches
- type inj_flags = {
- keep_proof_equalities : bool; (* One may want it or not *)
- injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *)
- injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *)
- }
-
- val build_selector :
- Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types ->
- EConstr.constr -> EConstr.constr -> EConstr.constr
- val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
- val general_rewrite :
- orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
- ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
- val inj : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag ->
- Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
- val general_multi_rewrite :
- Misctypes.evars_flag -> (bool * Misctypes.multi * Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings) list ->
- Locus.clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
- val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
- val replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic
- val dEq : keep_proofs:bool option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
- val discr_tac : Misctypes.evars_flag ->
- EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
- val injClause : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag ->
- EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
-
- val simpleInjClause : inj_flags option -> Misctypes.evars_flag ->
- EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option ->
- unit Proofview.tactic
- val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
- val rewriteInHyp : bool -> EConstr.constr -> Names.Id.t -> unit Proofview.tactic
- val cutRewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
- val cutRewriteInHyp : bool -> EConstr.types -> Names.Id.t -> unit Proofview.tactic
- val general_rewrite_ebindings_clause : Names.Id.t option ->
- orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
- ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic
- val subst : Names.Id.t list -> unit Proofview.tactic
-
- type subst_tactic_flags = {
- only_leibniz : bool;
- rewrite_dependent_proof : bool
- }
- val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic
-
- val general_rewrite_in :
- orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
- ?tac:(unit Proofview.tactic * conditions) -> Names.Id.t -> EConstr.constr -> Misctypes.evars_flag -> unit Proofview.tactic
-
- val general_setoid_rewrite_clause :
- (Names.Id.t option -> orientation -> Locus.occurrences -> EConstr.constr Misctypes.with_bindings ->
- new_goals:EConstr.constr list -> unit Proofview.tactic) Hook.t
-
- val discrConcl : unit Proofview.tactic
- val rewriteLR : ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
- val rewriteRL : ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
- val general_rewrite_bindings :
- orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
- ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic
- val discriminable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
- val discrHyp : Names.Id.t -> unit Proofview.tactic
- val injectable : Environ.env -> Evd.evar_map -> keep_proofs:(bool option) -> EConstr.constr -> EConstr.constr -> bool
- val injHyp : inj_flags option -> Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic
- val subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic
-end
-
-module Contradiction :
-sig
- val contradiction : EConstr.constr Misctypes.with_bindings option -> unit Proofview.tactic
- val absurd : EConstr.constr -> unit Proofview.tactic
-end
-
-module Inv :
-sig
- val dinv :
- Misctypes.inversion_kind -> EConstr.constr option ->
- Tactypes.or_and_intro_pattern option -> Misctypes.quantified_hypothesis -> unit Proofview.tactic
- val inv_clause :
- Misctypes.inversion_kind -> Tactypes.or_and_intro_pattern option -> Names.Id.t list ->
- Misctypes.quantified_hypothesis -> unit Proofview.tactic
- val inv_clear_tac : Names.Id.t -> unit Proofview.tactic
- val inv_tac : Names.Id.t -> unit Proofview.tactic
- val dinv_tac : Names.Id.t -> unit Proofview.tactic
- val dinv_clear_tac : Names.Id.t -> unit Proofview.tactic
- val inv : Misctypes.inversion_kind -> Tactypes.or_and_intro_pattern option ->
- Misctypes.quantified_hypothesis -> unit Proofview.tactic
-end
-
-module Leminv :
-sig
- val lemInv_clause :
- Misctypes.quantified_hypothesis -> EConstr.constr -> Names.Id.t list -> unit Proofview.tactic
- val add_inversion_lemma_exn :
- poly:bool -> Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) ->
- unit
-end
-
-module Hints :
-sig
-
- type raw_hint = EConstr.t * EConstr.types * Univ.ContextSet.t
-
- type 'a hint_ast =
- | Res_pf of 'a (* Hint Apply *)
- | ERes_pf of 'a (* Hint EApply *)
- | Give_exact of 'a
- | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
- | Unfold_nth of Names.evaluable_global_reference (* Hint Unfold *)
- | Extern of Genarg.glob_generic_argument (* Hint Extern *)
-
- type hint
-
- type debug =
- | Debug | Info | Off
-
- type 'a hints_path_atom_gen =
- | PathHints of 'a list
- | PathAny
-
- type hint_term =
- | IsGlobRef of Globnames.global_reference
- | IsConstr of EConstr.constr * Univ.ContextSet.t
-
- type hint_db_name = string
- type hint_info = (Names.Id.t list * Pattern.constr_pattern) Vernacexpr.hint_info_gen
- type hnf = bool
- type hints_path_atom = Globnames.global_reference hints_path_atom_gen
-
- type 'a hints_path_gen =
- | PathAtom of 'a hints_path_atom_gen
- | PathStar of 'a hints_path_gen
- | PathSeq of 'a hints_path_gen * 'a hints_path_gen
- | PathOr of 'a hints_path_gen * 'a hints_path_gen
- | PathEmpty
- | PathEpsilon
-
- type hints_path = Globnames.global_reference hints_path_gen
-
- type hints_entry =
- | HintsResolveEntry of (hint_info * Decl_kinds.polymorphic * hnf * hints_path_atom * hint_term) list
- | HintsImmediateEntry of (hints_path_atom * Decl_kinds.polymorphic * hint_term) list
- | HintsCutEntry of hints_path
- | HintsUnfoldEntry of Names.evaluable_global_reference list
- | HintsTransparencyEntry of Names.evaluable_global_reference list * bool
- | HintsModeEntry of Globnames.global_reference * Vernacexpr.hint_mode list
- | HintsExternEntry of hint_info * Genarg.glob_generic_argument
-
- type 'a with_metadata = private {
- pri : int;
- poly : Decl_kinds.polymorphic;
- pat : Pattern.constr_pattern option;
- name : hints_path_atom;
- db : string option;
- secvars : Names.Id.Pred.t;
- code : 'a;
- }
- type full_hint = hint with_metadata
-
- module Hint_db :
- sig
- type t
- val empty : ?name:hint_db_name -> Names.transparent_state -> bool -> t
- val transparent_state : t -> Names.transparent_state
- val iter : (Globnames.global_reference option ->
- Vernacexpr.hint_mode array list -> full_hint list -> unit) -> t -> unit
- end
- type hint_db = Hint_db.t
-
- val add_hints : bool -> hint_db_name list -> hints_entry -> unit
- val searchtable_map : hint_db_name -> hint_db
- val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
- val pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t
- val glob_hints_path_atom :
- Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
- val pp_hints_path : hints_path -> Pp.t
- val glob_hints_path :
- Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen
- val run_hint : hint ->
- ((raw_hint * Clenv.clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
- val typeclasses_db : hint_db_name
- val add_hints_init : (unit -> unit) -> unit
- val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit
- val empty_hint_info : 'a Vernacexpr.hint_info_gen
- val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast
- val pr_hint_db_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t
- val pr_hint_db : Hint_db.t -> Pp.t
- [@@ocaml.deprecated "please used pr_hint_db_env"]
-end
-
-module Auto :
-sig
- val default_auto : unit Proofview.tactic
- val full_trivial : ?debug:Hints.debug ->
- Tactypes.delayed_open_constr list -> unit Proofview.tactic
- val h_auto : ?debug:Hints.debug ->
- int option -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic
- val h_trivial : ?debug:Hints.debug ->
- Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic
- val new_full_auto : ?debug:Hints.debug ->
- int -> Tactypes.delayed_open_constr list -> unit Proofview.tactic
- val full_auto : ?debug:Hints.debug ->
- int -> Tactypes.delayed_open_constr list -> unit Proofview.tactic
- val new_auto : ?debug:Hints.debug ->
- int -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list -> unit Proofview.tactic
- val default_full_auto : unit Proofview.tactic
-end
-
-module Eauto :
-sig
- val e_assumption : unit Proofview.tactic
- val e_give_exact : ?flags:Unification.unify_flags -> EConstr.constr -> unit Proofview.tactic
- val prolog_tac : Tactypes.delayed_open_constr list -> int -> unit Proofview.tactic
- val make_dimension : int option -> int option -> bool * int
- val gen_eauto : ?debug:Hints.debug -> bool * int -> Tactypes.delayed_open_constr list ->
- Hints.hint_db_name list option -> unit Proofview.tactic
- val autounfold_tac : Hints.hint_db_name list option -> Locus.clause -> unit Proofview.tactic
- val autounfold_one : Hints.hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic
- val eauto_with_bases :
- ?debug:Hints.debug -> bool * int -> Tactypes.delayed_open_constr list -> Hints.hint_db list -> Proof_type.tactic
-end
-
-module Class_tactics :
-sig
-
- type search_strategy =
- | Dfs
- | Bfs
-
- val set_typeclasses_debug : bool -> unit
- val set_typeclasses_strategy : search_strategy -> unit
- val set_typeclasses_depth : int option -> unit
- val typeclasses_eauto : ?only_classes:bool -> ?st:Names.transparent_state -> ?strategy:search_strategy ->
- depth:(Int.t option) ->
- Hints.hint_db_name list -> unit Proofview.tactic
- val head_of_constr : Names.Id.t -> EConstr.constr -> unit Proofview.tactic
- val not_evar : EConstr.constr -> unit Proofview.tactic
- val is_ground : EConstr.constr -> unit Proofview.tactic
- val autoapply : EConstr.constr -> Hints.hint_db_name -> unit Proofview.tactic
- val catchable : exn -> bool
-end
-
-module Eqdecide :
-sig
- val compare : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
- val decideEqualityGoal : unit Proofview.tactic
-end
-
-module Autorewrite :
-sig
- type rew_rule = { rew_lemma: Constr.t;
- rew_type: Constr.types;
- rew_pat: Constr.t;
- rew_ctx: Univ.ContextSet.t;
- rew_l2r: bool;
- rew_tac: Genarg.glob_generic_argument option }
- type raw_rew_rule = (Constr.t Univ.in_universe_context_set * bool *
- Genarg.raw_generic_argument option)
- Loc.located
- val auto_multi_rewrite : ?conds:Equality.conditions -> string list -> Locus.clause -> unit Proofview.tactic
- val auto_multi_rewrite_with : ?conds:Equality.conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
- val add_rew_rules : string -> raw_rew_rule list -> unit
- val find_rewrites : string -> rew_rule list
- val find_matches : string -> Constr.t -> rew_rule list
- val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t
-end
-
-(************************************************************************)
-(* End of modules from tactics/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from vernac/ *)
-(************************************************************************)
-
-module Ppvernac :
-sig
- val pr_vernac : Vernacexpr.vernac_control -> Pp.t
- val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
-end
-
-module Lemmas :
-sig
-
- type 'a declaration_hook
-
- val mk_hook :
- (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
- val start_proof : Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Evd.evar_map ->
- ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val -> EConstr.types ->
- ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
- unit declaration_hook -> unit
- val call_hook :
- Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
- val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
- val get_current_context : unit -> Evd.evar_map * Environ.env
- [@@ocaml.deprecated "please use [Pfedit.get_current_context]"]
-end
-
-module Himsg :
-sig
- val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t
- val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t
-end
-
-module ExplainErr :
-sig
- val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
- val register_additional_error_info : (Util.iexn -> Pp.t option Loc.located option) -> unit
-end
-
-module Locality :
-sig
- val make_section_locality : bool option -> bool
- val make_module_locality : bool option -> bool
-end
-
-module Metasyntax :
-sig
-
- val add_token_obj : string -> unit
-
- type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
- val register_grammar : string -> any_entry list -> unit
-
-end
-
-module Search :
-sig
- type glob_search_about_item =
- | GlobSearchSubPattern of Pattern.constr_pattern
- | GlobSearchString of string
- type filter_function = Globnames.global_reference -> Environ.env -> Constr.t -> bool
- type display_function = Globnames.global_reference -> Environ.env -> Constr.t -> unit
- val search_about_filter : glob_search_about_item -> filter_function
- val module_filter : Names.DirPath.t list * bool -> filter_function
- val generic_search : int option -> display_function -> unit
-end
-
-module Obligations :
-sig
- val default_tactic : unit Proofview.tactic ref
- val obligation : int * Names.Id.t option * Constrexpr.constr_expr option ->
- Genarg.glob_generic_argument option -> unit
- val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> unit
- val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit
- val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> unit
- val solve_all_obligations : unit Proofview.tactic option -> unit
- val admit_obligations : Names.Id.t option -> unit
- val show_obligations : ?msg:bool -> Names.Id.t option -> unit
- val show_term : Names.Id.t option -> Pp.t
-end
-
-module ComDefinition :
-sig
- val do_definition :
- program_mode:bool ->
- Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
- Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr ->
- Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit
-end
-
-module ComFixpoint :
-sig
-
- open Names
- open Constrexpr
-
- type structured_fixpoint_expr = {
- fix_name : Id.t;
- fix_univs : Vernacexpr.universe_decl_expr option;
- fix_annot : Id.t Loc.located option;
- fix_binders : local_binder_expr list;
- fix_body : constr_expr option;
- fix_type : constr_expr
- }
-
- type recursive_preentry = Names.Id.t list * Constr.t option list * Constr.types list
-
- val interp_fixpoint :
- cofix:bool ->
- structured_fixpoint_expr list -> Vernacexpr.decl_notation list ->
- recursive_preentry * Univdecls.universe_decl * UState.t *
- (EConstr.rel_context * Impargs.manual_implicits * int option) list
-
- val extract_fixpoint_components : bool ->
- (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
- structured_fixpoint_expr list * Vernacexpr.decl_notation list
-
- val do_fixpoint :
- Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit
-
-end
-
-module ComInductive :
-sig
- open Names
- open Constrexpr
- open Vernacexpr
-
- type structured_one_inductive_expr = {
- ind_name : Id.t;
- ind_univs : universe_decl_expr option;
- ind_arity : constr_expr;
- ind_lc : (Id.t * constr_expr) list
- }
-
- type structured_inductive_expr =
- local_binder_expr list * structured_one_inductive_expr list
-
- type one_inductive_impls
-
- val do_mutual_inductive :
- (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
- Decl_kinds.private_flag -> Declarations.recursivity_kind -> unit
-
- val extract_mutual_inductive_declaration_components :
- (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list ->
- structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list
-
- val interp_mutual_inductive :
- structured_inductive_expr -> Vernacexpr.decl_notation list ->
- Decl_kinds.cumulative_inductive_flag ->
- Decl_kinds.polymorphic ->
- Decl_kinds.private_flag -> Declarations.recursivity_kind ->
- Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
-
- val declare_mutual_inductive_with_eliminations :
- Entries.mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
- Names.MutInd.t
-end
-
-module Classes :
-sig
- val set_typeclass_transparency : Names.evaluable_global_reference -> bool -> bool -> unit
- val new_instance :
- ?abstract:bool ->
- ?global:bool ->
- ?refine:bool ->
- program_mode:bool ->
- Decl_kinds.polymorphic ->
- Constrexpr.local_binder_expr list ->
- Vernacexpr.typeclass_constraint ->
- (bool * Constrexpr.constr_expr) option ->
- ?generalize:bool ->
- ?tac:unit Proofview.tactic ->
- ?hook:(Globnames.global_reference -> unit) ->
- Vernacexpr.hint_info_expr ->
- Names.Id.t
-end
-
-module Vernacstate :
-sig
-
- type t = {
- system : States.state; (* summary + libstack *)
- proof : Proof_global.t; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
- }
-
- (* XXX: This should not be exported *)
- val freeze_interp_state : Summary.marshallable -> t
- val unfreeze_interp_state : t -> unit
-
-end
-
-module Vernacinterp :
-sig
-
- type deprecation = bool
-
- type atts = {
- loc : Loc.t option;
- locality : bool option;
- polymorphic : bool;
- }
-
- type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
-
- type plugin_args = Genarg.raw_generic_argument list
-
- val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
-
-end
-
-module Mltop :
-sig
- val declare_cache_obj : (unit -> unit) -> string -> unit
- val add_known_plugin : (unit -> unit) -> string -> unit
- val add_known_module : string -> unit
- val module_is_known : string -> bool
-end
-
-module Topfmt :
-sig
- val std_ft : Format.formatter ref
- val with_output_to : out_channel -> Format.formatter
- val get_margin : unit -> int option
-end
-
-module Vernacentries :
-sig
-
- val dump_global : Libnames.reference Misctypes.or_by_notation -> unit
- val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
- Evd.evar_map * Redexpr.red_expr) Hook.t
- val command_focus : unit Proof.focus_kind
-end
-
-(************************************************************************)
-(* End of modules from vernac/ *)
-(************************************************************************)
-
-(************************************************************************)
-(* Modules from stm/ *)
-(************************************************************************)
-
-module Vernac_classifier :
-sig
- val declare_vernac_classifier :
- Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> Vernacexpr.vernac_classification) -> unit
- val classify_as_proofstep : Vernacexpr.vernac_classification
- val classify_as_query : Vernacexpr.vernac_classification
- val classify_as_sideeff : Vernacexpr.vernac_classification
- val classify_vernac : Vernacexpr.vernac_control -> Vernacexpr.vernac_classification
-end
-
-module Stm :
-sig
- type doc
-
- val get_doc : Feedback.doc_id -> doc
-
- val state_of_id : doc:doc ->
- Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ]
-end
-
-(************************************************************************)
-(* End of modules from stm/ *)
-(************************************************************************)
diff --git a/API/API.mllib b/API/API.mllib
deleted file mode 100644
index 25275c704..000000000
--- a/API/API.mllib
+++ /dev/null
@@ -1 +0,0 @@
-API
diff --git a/API/PROPERTIES b/API/PROPERTIES
deleted file mode 100644
index cd942e202..000000000
--- a/API/PROPERTIES
+++ /dev/null
@@ -1,8 +0,0 @@
-0 : All API elements, i.e.:
- - modules
- - module types
- - functions & values
- - types
- are present if and only if are needed for implementing Coq plugins.
-
-1 : Individual API elements are not aliased.
diff --git a/META.coq b/META.coq
index 75cec8f0c..76d5b4147 100644
--- a/META.coq
+++ b/META.coq
@@ -240,25 +240,12 @@ package "stm" (
)
-package "API" (
-
- description = "Coq API"
- version = "8.7"
-
- requires = "coq.intf, coq.stm"
- directory = "API"
-
- archive(byte) = "API.cma"
- archive(native) = "API.cmxa"
-
-)
-
package "ltac" (
description = "Coq LTAC Plugin"
version = "8.7"
- requires = "coq.API"
+ requires = "coq.stm"
directory = "plugins/ltac"
archive(byte) = "ltac_plugin.cmo"
diff --git a/Makefile.build b/Makefile.build
index 33ab72e68..9a838b85c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -195,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
COQOPTS=$(NATIVECOMPUTE)
BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
-LOCALINCLUDES=$(if $(filter plugins/%,$@),-I clib -I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS)))
+LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
@@ -576,12 +576,6 @@ kernel/kernel.cma: kernel/kernel.mllib
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
-# Specific rule for API/API.cmi
-# Make sure that API/API.mli cannot leak types from the Coq codebase.
-API/API.cmi : API/API.mli
- $(SHOW)'OCAMLC $<'
- $(HIDE)$(OCAMLC) -I clib -I lib -I $(MYCAMLP4LIB) -c $<
-
%.cma: %.mllib
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
diff --git a/Makefile.common b/Makefile.common
index 7e8f3e3e7..d3a9b0b96 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -75,7 +75,7 @@ MKDIR:=install -d
CORESRCDIRS:=\
config clib lib kernel intf kernel/byterun library \
engine pretyping interp proofs parsing printing \
- tactics vernac stm toplevel API
+ tactics vernac stm toplevel
PLUGINDIRS:=\
omega romega micromega quote \
@@ -103,7 +103,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
- stm/stm.cma toplevel/toplevel.cma API/API.cma
+ stm/stm.cma toplevel/toplevel.cma
TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
diff --git a/Makefile.dev b/Makefile.dev
index d2a1e9235..db83be369 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -119,7 +119,7 @@ pretyping: pretyping/pretyping.cma
stm: stm/stm.cma
toplevel: toplevel/toplevel.cma
-.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping API
+.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
.PHONY: engine stm toplevel
######################
diff --git a/Makefile.doc b/Makefile.doc
index 1b0803f19..8cb9c9f0f 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -387,7 +387,7 @@ OCAMLDOCDIR=dev/ocamldoc
DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \
- ./parsing/*.mli ./proofs/*.mli API/API.mli \
+ ./parsing/*.mli ./proofs/*.mli \
./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli)
# Defining options to generate dependencies graphs
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 1666df0bd..e2d9d0d01 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -52,7 +52,6 @@ val vo_magic_number : int
val state_magic_number : int
val core_src_dirs : string list
-val api_dirs : string list
val plugins_dirs : string list
val all_src_dirs : string list
diff --git a/configure.ml b/configure.ml
index 0698d93e2..a86b78ba5 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1134,7 +1134,7 @@ let write_configml f =
pr_b "bytecode_compiler" !Prefs.bytecodecompiler;
pr_b "native_compiler" !Prefs.nativecompiler;
- let core_src_dirs = [ "config"; "dev"; "kernel"; "library";
+ let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library";
"engine"; "pretyping"; "interp"; "parsing"; "proofs";
"tactics"; "toplevel"; "printing"; "intf";
"grammar"; "ide"; "stm"; "vernac" ] in
@@ -1143,7 +1143,6 @@ let write_configml f =
core_src_dirs in
pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs;
- pr "\nlet api_dirs = [\"API\"; \"clib\"; \"lib\"]\n";
pr "\nlet plugins_dirs = [\n";
let plugins = Sys.readdir "plugins" in
@@ -1155,7 +1154,7 @@ let write_configml f =
plugins;
pr "]\n";
- pr "\nlet all_src_dirs = core_src_dirs @ api_dirs @ plugins_dirs\n";
+ pr "\nlet all_src_dirs = core_src_dirs @ plugins_dirs\n";
close_out o;
Unix.chmod f 0o444
diff --git a/dev/base_include b/dev/base_include
index 4dc9a0bee..2a4ad4a15 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -18,12 +18,10 @@
#directory "intf";;
#directory "stm";;
#directory "vernac";;
-#directory "../API";;
#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
-#load "API.cma";;
#use "top_printers.ml";;
#use "vm_printers.ml";;
@@ -194,7 +192,7 @@ let qid = Libnames.qualid_of_string;;
let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
-let parse_tac = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
+let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
(* build a term of type glob_constr without type-checking or resolution of
implicit syntax *)
diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh
new file mode 100644
index 000000000..9677b3525
--- /dev/null
+++ b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh
@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then
+ Equations_CI_BRANCH=API-removal
+ Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git
+ coq_dpdgraph_CI_BRANCH=API-removal
+ coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git
+ ltac2_CI_BRANCH=API-removal
+ ltac2_CI_GITURL=https://github.com/gares/ltac2.git
+fi
diff --git a/dev/core.dbg b/dev/core.dbg
index 18e82c352..00a4355a4 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -17,5 +17,4 @@ load_printer vernac.cma
load_printer stm.cma
load_printer toplevel.cma
load_printer intf.cma
-load_printer API.cma
load_printer ltac_plugin.cmo
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index f6fbb6942..e616bd566 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -12,16 +12,6 @@ All the bugs with a number below 1154 had to be renumbered, you can find
a correspondence table [here](/dev/bugzilla2github_stripped.csv).
All the other bugs kept their number.
-### Plugin API
-
-Coq 8.8 offers a new module overlay containing a proposed plugin API
-in `API/API.ml`; this overlay is enabled by adding the `-open API`
-flag to the OCaml compiler; this happens automatically for
-developments in the `plugin` folder and `coq_makefile`.
-
-However, `coq_makefile` can be instructed not to enable this flag by
-passing `-bypass-API`.
-
### ML API
General deprecation
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index f4799f7b2..3850c05fd 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -23,7 +23,6 @@ exec $OCAMLDEBUG \
-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
-I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
- -I $COQTOP/API \
-I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \
-I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
-I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 832040ad2..ff3825787 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -233,7 +233,7 @@ let ppenvwithcst e = pp
str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
-let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (API.Global.env()) x))
+let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
let ppobj obj = Format.print_string (Libobject.object_tag obj)
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 34f9aed37..1e52af0be 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -11,7 +11,6 @@ type project = {
makefile : string option;
install_kind : install option;
use_ocamlopt : bool;
- bypass_API : bool;
v_files : string list;
mli_files : string list;
@@ -43,12 +42,11 @@ and install =
| UserInstall
(* TODO generate with PPX *)
-let mk_project project_file makefile install_kind use_ocamlopt bypass_API = {
+let mk_project project_file makefile install_kind use_ocamlopt = {
project_file;
makefile;
install_kind;
use_ocamlopt;
- bypass_API;
v_files = [];
mli_files = [];
@@ -181,8 +179,6 @@ let process_cmd_line orig_dir proj args =
aux { proj with defs = proj.defs @ [v,def] } r
| "-arg" :: a :: r ->
aux { proj with extra_args = proj.extra_args @ [a] } r
- | "-bypass-API" :: r ->
- aux { proj with bypass_API = true } r
| f :: r ->
let f = CUnix.correct_path f orig_dir in
let proj =
@@ -202,11 +198,11 @@ let process_cmd_line orig_dir proj args =
(******************************* API ************************************)
let cmdline_args_to_project ~curdir args =
- process_cmd_line curdir (mk_project None None None true false) args
+ process_cmd_line curdir (mk_project None None None true) args
let read_project_file f =
process_cmd_line (Filename.dirname f)
- (mk_project (Some f) None (Some NoInstall) true false) (parse f)
+ (mk_project (Some f) None (Some NoInstall) true) (parse f)
let rec find_project_file ~from ~projfile_name =
let fname = Filename.concat from projfile_name in
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 23a27a54a..810189450 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -13,7 +13,6 @@ type project = {
makefile : string option;
install_kind : install option;
use_ocamlopt : bool;
- bypass_API : bool;
v_files : string list;
mli_files : string list;
diff --git a/plugins/.merlin b/plugins/.merlin
index dd6678ba0..2ba616962 100644
--- a/plugins/.merlin
+++ b/plugins/.merlin
@@ -1,2 +1 @@
REC
-FLG -open API
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 363ad5dfc..8fe05b497 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -861,7 +861,7 @@ let rec prove_le g =
| App (c, [| x0 ; _ |]) ->
EConstr.isVar sigma x0 &&
Id.equal (destVar sigma x0) (destVar sigma x) &&
- is_global sigma (le ()) c
+ EConstr.is_global sigma (le ()) c
| _ -> false
in
let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 169ac5c90..55c519e24 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -23,7 +23,7 @@ val tclORELSE0 : tactic -> tactic -> tactic
val tclORELSE : tactic -> tactic -> tactic
val tclTHEN : tactic -> tactic -> tactic
val tclTHENSEQ : tactic list -> tactic
-[@@ocaml.deprecated "alias of API.Tacticals.tclTHENLIST"]
+[@@ocaml.deprecated "alias of Tacticals.tclTHENLIST"]
val tclTHENLIST : tactic list -> tactic
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
val tclTHENFIRST : tactic -> tactic -> tactic
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
deleted file mode 100755
index e48f704a2..000000000
--- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
+++ /dev/null
@@ -1,36 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-cat > _CoqProject <<EOT
--I src/
-
-./src/test_plugin.mllib
-./src/test.ml4
-./src/test.mli
-EOT
-
-mkdir -p src
-
-cat > src/test_plugin.mllib <<EOT
-Test
-EOT
-
-touch src/test.mli
-
-cat > src/test.ml4 <<EOT
-DECLARE PLUGIN "test"
-
-let _ = Pre_env.empty_env
-EOT
-
-${COQBIN}coq_makefile -f _CoqProject -o Makefile
-cat Makefile.conf
-
-if make VERBOSE=1; then
- # make command should have failed (but didn't)
- exit 1
-else
- # make command should have failed (and it indeed did)
- exit 0
-fi
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
deleted file mode 100755
index 4a8f58655..000000000
--- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
+++ /dev/null
@@ -1,31 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-cat > _CoqProject <<EOT
--bypass-API
--I src/
-
-./src/test_plugin.mllib
-./src/test.ml4
-./src/test.mli
-EOT
-
-mkdir -p src
-
-cat > src/test_plugin.mllib <<EOT
-Test
-EOT
-
-touch src/test.mli
-
-cat > src/test.ml4 <<EOT
-DECLARE PLUGIN "test"
-
-let _ = Pre_env.empty_env
-EOT
-
-${COQBIN}coq_makefile -f _CoqProject -o Makefile
-cat Makefile.conf
-
-make VERBOSE=1
diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4
index e7d0bfe1f..72765abe0 100644
--- a/test-suite/coq-makefile/template/src/test.ml4
+++ b/test-suite/coq-makefile/template/src/test.ml4
@@ -1,4 +1,3 @@
-open API
open Ltac_plugin
DECLARE PLUGIN "test_plugin"
let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml
index e134abd84..a01d0865a 100644
--- a/test-suite/coq-makefile/template/src/test_aux.ml
+++ b/test-suite/coq-makefile/template/src/test_aux.ml
@@ -1 +1 @@
-let tac = API.Proofview.tclUNIT ()
+let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli
index 2e7ad1529..10020f27d 100644
--- a/test-suite/coq-makefile/template/src/test_aux.mli
+++ b/test-suite/coq-makefile/template/src/test_aux.mli
@@ -1 +1 @@
-val tac : unit API.Proofview.tactic
+val tac : unit Proofview.tactic
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 33a2f8593..de113df6a 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -176,7 +176,7 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@
COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
-CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS)
+CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
# ocamldoc fails with unknown argument otherwise
CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b7a62a78c..091869407 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -57,7 +57,6 @@ let usage_common () =
\n[-install opt]: where opt is \"user\" to force install into user directory,\
\n \"none\" to build a makefile with no install target or\
\n \"global\" to force install in $COQLIB directory\
-\n[-bypass-API]: when compiling plugins, bypass Coq API\
\n"
let usage_coq_project () =
@@ -210,16 +209,10 @@ let windrive s =
else s
;;
-let generate_conf_coq_config oc args bypass_API =
+let generate_conf_coq_config oc args =
section oc "Coq configuration.";
- let src_dirs = if bypass_API
- then Coq_config.all_src_dirs
- else Coq_config.api_dirs @ Coq_config.plugins_dirs in
+ let src_dirs = Coq_config.all_src_dirs in
Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
- if bypass_API then
- Printf.fprintf oc "OCAML_API_FLAGS=\n"
- else
- Printf.fprintf oc "OCAML_API_FLAGS=-open API\n";
fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib)
;;
@@ -278,7 +271,7 @@ let generate_conf oc project args =
fprintf oc "# %s\n\n" (String.concat " " (List.map quote args));
generate_conf_files oc project;
generate_conf_includes oc project;
- generate_conf_coq_config oc args project.bypass_API;
+ generate_conf_coq_config oc args;
generate_conf_defs oc project;
generate_conf_doc oc project;
generate_conf_extra_target oc project.extra_targets;