On This Page
- The type of constructions
- Functions for dealing with constr terms.
- Term constructors.
- Concrete type for making pattern-matching.
- Term destructors
- Equality
- Extension of Context with declarations on constr
- Relocation and substitution
- Functionals working on expressions canonically abstracted over a local context (possibly with let-ins)
- Functionals working on the immediate subterm of a construction
- Hashconsing
package coq-core
-
coq-core.clib
-
coq-core.config
-
coq-core.coqworkmgrapi
-
coq-core.engine
-
coq-core.interp
-
coq-core.kernel
-
coq-core.lib
-
coq-core.library
-
coq-core.perf
-
coq-core.plugins.btauto
-
coq-core.plugins.derive
-
coq-core.plugins.extraction
-
coq-core.plugins.ltac
-
-
coq-core.plugins.ltac2
-
-
coq-core.plugins.micromega
-
-
coq-core.plugins.number_string_notation
-
coq-core.plugins.ring
-
coq-core.plugins.rtauto
-
coq-core.plugins.ssreflect
-
coq-core.plugins.ssrmatching
-
coq-core.plugins.tauto
-
coq-core.plugins.tutorial.p0
-
coq-core.plugins.tutorial.p1
-
coq-core.plugins.tutorial.p2
-
coq-core.plugins.tutorial.p3
-
coq-core.pretyping