aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
AgeCommit message (Collapse)Author
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: ppedrot
2021-03-26Add an Ltac1 to Ltac2 FFI for identifiers.Pierre-Marie Pédrot
Before you ask, the Ltac2.Ltac1 module is voluntarily underdocumented. Fixes #13996: missing Ltac1.to_ident.
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
Previously, `Array.init` was computing the first element of the array twice, resulting in exponential overhead in the number of recursive nestings of `Array.init`. Notably, since `Array.map` is implemented in terms of `Array.init`, this exponential blowup shows up in any term traversal based on `Array.map` over the arguments of application nodes. Fixes #14011
2021-03-25Fix the redeclaration check for Ltac2 entry points.Pierre-Marie Pédrot
Fixes #14003: Ltac2 redefinition check is broken.
2021-03-25Merge PR #13989: fix documentation of Ltac2.Env.expandPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: ppedrot
2021-03-24Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-24Merge PR #13973: Factorize goal selector handlingPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵Michael Soegtrop
notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2021-03-23fix documentation of Ltac2.Env.expandSamuel Gruetter
2021-03-22Factorize goal selector handlingGaëtan Gilbert
As a bonus ltac2 can produce bullet suggestions.
2021-03-19implement is_const, is_var, ... etc and has_evar for Ltac2Samuel Gruetter
Fixes #13963
2021-03-18Implement ! goal selector for Ltac2.Pierre-Marie Pédrot
Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
2021-03-17Merge PR #13938: Fast Ltac2 quoted variable typingcoqbot-app[bot]
Reviewed-by: gares
2021-03-16Slightly richer API allowing to shift the inductive in a block.Pierre-Marie Pédrot
2021-03-16Adding an Ltac2 API to manipulate inductive types.Pierre-Marie Pédrot
Fixes #10095: Get list of constructors of Inductive.
2021-03-12Use the new API to prevent retyping of Ltac2 variable quotations.Pierre-Marie Pédrot
Fixes #12785: Ltac2 Performance Overhead.
2021-03-12Move the responsibility of type-checking to the caller for tactic-in-terms.Pierre-Marie Pédrot
Instead of taking a type and checking that the inferred type for the expression is correct, we simply pick an optional constraint and return the type directly in the callback. This prevents having to compute type conversion twice in the special case of Ltac2 variable quotations. This should be 1:1 equivalent to the previous code, we are just moving code around.
2021-03-10Allow to register deprecation status in Ltac2 term and notation declarations.Pierre-Marie Pédrot
2021-03-10Allow the presence of type casts for return values in Ltac2.Pierre-Marie Pédrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
Reviewed-by: JasonGross Reviewed-by: MSoegtropIMC
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
2021-01-22Add a type of format strings to Ltac2.Pierre-Marie Pédrot
It provides an abstract type of well-typed format strings, a scope to parse them and a minimal printf-like API.
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` ↵Pierre-Marie Pédrot
into `pat:` Ack-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval.
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
It is the only place where it starts making sense in the whole codebase. It also fits nicely there since there are other functions manipulating this type in that module. In any case this type does not belong to the kernel.
2020-12-04turn Ltac2's `pattern:` into `pat:`Kenji Maillard
2020-11-30Add an abstraction function in the LtacX FFI.Pierre-Marie Pédrot
This allows to embed Ltac2 functions manipulating Ltac1 values as simple Ltac1 values.
2020-11-30Store Ltac2 valexpr instead of unevaluated code inside Ltac1 value embedding.Pierre-Marie Pédrot
This should have the same semantics, it is just a matter of moving the responsibility of evaluating the thunk from the Ltac1 application tactic to the quotation.
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
This allows proper treatment in notations, ie fixes #13303 The "glob" representation of universes (what pretyping sees) contains only fully interpreted (kernel) universes and unbound universe ids (for non Strict Universe Declaration). This means universes need to be understood at intern time, so intern now has a new "universe binders" argument. We cannot avoid this due to the following example: ~~~coq Module Import M. Universe i. End M. Definition foo@{i} := Type@{i}. ~~~ When interning `Type@{i}` we need to know that `i` is locally bound to avoid interning it as `M.i`. Extern has a symmetrical problem: ~~~coq Module Import M. Universe i. End M. Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}. Print foo. (* must not print Type@{i} -> Type@{i} *) ~~~ (Polymorphic as otherwise the local `i` will be called `foo.i`) Therefore extern also takes a universe binders argument. Note that the current implementation actually replaces local universes with names at detype type. (Asymmetrical to pretyping which only gets names in glob terms for dynamically declared univs, although it's capable of understanding bound univs too) As such extern only really needs the domain of the universe binders (ie the set of bound universe ids), we just arbitrarily pass the whole universe binders to avoid putting `Id.Map.domain` at every entry point. Note that if we want to change so that detyping does not name locally bound univs we would need to pass the reverse universe binders (map from levels to ids, contained in the ustate ie in the evar map) to extern.
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-04Adding an if-then-else syntax to Ltac2.Pierre-Marie Pédrot
This is a syntactic sugar that is compiled away to a simple case analysis.
2020-10-27Rename tac2type -> ltac2_type,Jim Fehrle
typ_param -> ltac2_typevar, tac2expr -> ltac2_expr
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-26Ltac2: use ComTactic infrastructureGaëtan Gilbert
2020-10-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-11Turn integer into natural in several mlgsPierre Roux
Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 .
2020-07-18Clarify the Ltac2 invalid identifier message.Pierre-Marie Pédrot
2020-07-18Better location for match! pattern variables in Ltac2.Pierre-Marie Pédrot
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: proux01 Ack-by: silene
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-05Merge PR #12594: Fix ltac2 type parametersMichael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: gares
2020-07-01Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t.Pierre-Marie Pédrot
It seems that nobody tried to write a parameterized type with more than one parameter since this was causing a syntax error. LL(1) being great, we work around the issue by factorizing the syntax with the generic parentheses and decide the validity after parsing.
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
At this point the record in lemmas was just a stub; next commit will stop exposing the internals of mutual information, and pave the way for the refactoring of `Info.t` handling in the Declare interface.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 21:46:07 +0000