aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| | | | | | | | | | We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* \ Merge PR #6248: [api] Remove aliases of `Evar.t`Gravatar Maxime Dénès2017-11-28
|\ \
| * | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| | | | | | | | | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function.
* | | Use Evarutil.has_undefined_evars for tactic has_evar.Gravatar Gaëtan Gilbert2017-11-24
|/ /
| * Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean.
| * When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
| * Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former).
| * Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
|/
* Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingGravatar Maxime Dénès2017-11-24
|\
* \ Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Gravatar Maxime Dénès2017-11-24
|\ \ | | | | | | | | | constructs.
* \ \ Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionGravatar Maxime Dénès2017-11-24
|\ \ \
* \ \ \ Merge PR #6197: [plugin] Remove LocalityFixme über hack.Gravatar Maxime Dénès2017-11-24
|\ \ \ \
| | | * | Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
* | | | | Merge PR #6186: [api] Miscellaneous consolidation.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \ | |_|_|/ / |/| | | |
| | | * | Recognizing Z in romega up to conversion.Gravatar Hugo Herbelin2017-11-23
| | | | |
| | | * | Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Gravatar Hugo Herbelin2017-11-23
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
| | | * Fixing a 8.7 regression of ring_simplify in ArithRing.Gravatar Hugo Herbelin2017-11-23
| |_|/ |/| | | | | | | | | | | With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191).
* | | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Maxime Dénès2017-11-23
|\ \ \
| | | * [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it.
| | * [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | | | | | | | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
| | * [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
| |/ |/| | | | | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
* | [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
| | | | | | | | | | | | | | | | | | | | | | We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear.
* | Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Maxime Dénès2017-11-21
|\ \
* \ \ Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesGravatar Maxime Dénès2017-11-21
|\ \ \
| * | | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
| | | | | | | | | | | | | | | | Was broken since 8.6.
* | | | Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Gravatar Maxime Dénès2017-11-20
|\ \ \ \
* \ \ \ \ Merge PR #6161: Fix micromega.ml to match generated file and enforce match ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | in make.
| | | | | * Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Gaëtan Gilbert2017-11-19
| |_|_|_|/ |/| | | |
| | * | | [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state.
| | | * [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I followed what seems to be the intention of the code, with the original intention of remove the global imperative proof state. However, I fully fail to see why the new API is better than the old one. In fact the opposite seems the contrary. Still big parts of the "new proof engine" seem unfinished, and I'm afraid I am not the right person to know what direction things should take.
* | | Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.Gravatar Maxime Dénès2017-11-16
|\ \ \
* \ \ \ Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2Gravatar Maxime Dénès2017-11-16
|\ \ \ \
| | | * | Fix micromega.ml to match generated file and enforce match in make.Gravatar Gaëtan Gilbert2017-11-16
| |_|/ / |/| | | | | | | | | | | Mismatch probably caused by c5aca4005.
| | | * Fixing printing of tactics encapsulated as tacarg with Tacexp.Gravatar Hugo Herbelin2017-11-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We preserve the level instead of resetting it at level 0. Probably it would be the same as giving level ltop since Tacexp apparently comes only from using a tactic in an Ltac "let", which is where I observed a problem.
| | | * Using "l" printer for glob_constr, like for constr.Gravatar Hugo Herbelin2017-11-15
| |_|/ |/| | | | | | | | | | | This is to avoid excessive parentheses, in particular when printing "constr:()" in "Print Ltac f".
| | * [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
| |/ |/|
* | Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\ \
| * | [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | | | | | | | | | We do up to `Term` which is the main bulk of the changes.
* | | Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Hugo Herbelin2017-11-04
|/ / | | | | | | Adding a file fixing #5996 and which uses this feature.
* | Merge PR #6047: A generic printer for ltac valuesGravatar Maxime Dénès2017-11-03
|\ \
* \ \ Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Maxime Dénès2017-11-03
|\ \ \
| | * | Ltac Debug: exporting env and sigma when needed so that term can be printed.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We do it so as to preserve non-focussing semantics for non-focussing generic arguments. This assumes that the code treats them consistently, which is not enforced statically, but which is reasonable in the sense that when we need a context for printing, we have no other choice as needing a context and we needed one also at interpretation time.
| | * | Binding ltac printing functions to the system of generic printing.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786.
| | * | Setting a system to register printers for Ltac values.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The model provides three kinds of printers depending on whether the printer needs a context, and, if yes if it supports levels. In the latter case, it takes defaults levels for printing when in a surrounded context (lconstr style) and for printing when not in a surrounded context (constr style). This model preserves the 8.7 focussing semantics of "idtac" (i.e. focussing only when an env is needed) but it also shows that the semantics of "idtac", which focusses the goal depending on the type of its arguments, is a bit ad hoc to understand. See discussion at PR#6047 "https://github.com/coq/coq/pull/6047#discussion_r148278454".
| | * | Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
| | | |
| | * | Exporting a few more printing functions.Gravatar Hugo Herbelin2017-11-02
| | | |
| | * | Improving checks about the list separator in tactic notations.Gravatar Hugo Herbelin2017-11-02
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | In Tactic Notation and TACTIC EXTEND, when an argument not ending with "_list_sep" was given with a separator, the separator was silently ignored. Now: - we take it into account if it is a list (i.e. ending with "_list"), as if "_list_sep" was given, since after all, the "_sep" is useless in the name. - we fail if there is a separator but it is not a "_list" or "_list_sep".
| * | Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Hugo Herbelin2017-10-30
| | | | | | | | | | | | | | | | | | We fix by interpreting the pattern in "change pat with term" in strict mode by using the same interning code as for "match goal" (even if the pattern is dropped afterwards).
* | | Merge PR #6015: [general] Remove Econstr dependency from `intf`Gravatar Maxime Dénès2017-10-27
|\ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 08:01:47 +0000