aboutsummaryrefslogtreecommitdiff
path: root/API
AgeCommit message (Collapse)Author
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.
2017-10-10Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Maxime Dénès
2017-10-09Merge PR #1087: [stm] Switch to a functional APIMaxime Dénès
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
We make the Stm API functional over an opaque `doc` type. This allows to have a much better picture of what the toplevel is doing; now almost all users of STM private data are marked by typing. For now only, the API is functional; a PR switching the internals should come soon thou; however we must first fix some initialization bugs. Due to some users, we modify `feedback` internally to include a "document id" field; we don't expose this change in the IDE protocol yet.
2017-10-05romega: takes advantage of context variables with bodyPierre Letouzey
When a context variable x is of the form "x := body : Z", romega is now made aware of this body. Technically, we reify an equation x = body, and push a corresponding (eq_refl x) as argument of the final do_omega. See also the previous commit adding this same feature to omega (fixing bug 142).
2017-10-03Ltac uses the new generic locatable API.Pierre-Marie Pédrot
2017-10-03Moving the Ltac-specific part of the nametab to the Ltac plugin.Pierre-Marie Pédrot
For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit.
2017-10-03Merge PR #1040: Efficient fresh name generationMaxime Dénès
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-19Remove STM vernaculars.Maxime Dénès
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
2017-09-15Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Maxime Dénès
top of the linking chain.
2017-09-15Merge PR #1051: Using an algebraic type for distinguishing toplevel input ↵Maxime Dénès
from location in file
2017-09-15Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Maxime Dénès
2017-09-14Using an algebraic type for distinguishing toplevel input from location in file.Hugo Herbelin
2017-09-12Port is_Set and is_Type to EConstr, as was is_Prop already.Guillaume Melquiond
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family.
2017-09-07Merge PR #931: Parametrize module bodyMaxime Dénès
2017-09-07Merge PR #914: Making the detyper lazyMaxime Dénès
2017-09-07Merge PR #904: Add build_coq_or to API.CoqlibMaxime Dénès
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
2017-08-29[general] Merge parsing with highparsing, put toplevel at the top of the ↵Emilio Jesus Gallego Arias
linking chain.
2017-08-29[vernac] Store Infix Modifier in Vernac Notation.Pierre-Marie Pédrot
This removes a dependency from `G_vernac` to `Metasyntax`.
2017-08-29Statically enforcing that module types have no retroknowledge.Pierre-Marie Pédrot
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
As explained in edf85b9, the original commit that merged the module_body and module_type_body representations, this was delayed to a later time assumedly due to OCaml lack of GADTs. Actually, the only thing that was needed was polymorphic recursion, which has been around already for a relatively long time (since 3.12).
2017-08-29Post-merge API fix.Maxime Dénès
2017-08-29Merge PR #946: Functional pretyping interfaceMaxime Dénès
2017-08-29Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵Maxime Dénès
restructuration
2017-08-29Merge PR #805: Functional tacticsMaxime Dénès
2017-08-29A new step of restructuration of notations.Hugo Herbelin
This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20).
2017-08-18Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict ↵Maxime Dénès
with OCaml.
2017-08-16Merge PR #912: Detyping functions are now operating on EConstr.t.Maxime Dénès
2017-08-16Merge PR #864: Some cleanups after cumulativity for inductive typesMaxime Dénès
2017-08-12Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Hugo Herbelin
Indeed OCaml has a similar file and this conflicts, at least in debugger.
2017-08-07Add build_coq_or to APISigurd Schneider
2017-08-01Move type_uconstr to Tacinterp.Maxime Dénès
2017-08-01Remove pure_open_constr (now open_constr)Maxime Dénès
2017-08-01Detyping functions are now operating on EConstr.t.Pierre-Marie Pédrot
This was already the case, but the API was not exposing this.
2017-08-01Move glob_constr_ltac_closure to evar_refiner.Maxime Dénès
2017-08-01Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Maxime Dénès
2017-07-31Improve errors for cumulativity when monomorphicAmin Timany
We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic.
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-31Correcting [build_discriminator] to make the test-suite passamblaf
2017-07-28Merge PR #889: Removing template polymorphism for definitions.Maxime Dénès
2017-07-28Merge PR #888: Stronger kernel typesMaxime Dénès
2017-07-28Merge PR #782: Update API for fiatMaxime Dénès
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 04:09:51 +0000