aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Collapse)AuthorAge
...
| | * | Remove reference name type.Gravatar Maxime Dénès2018-06-18
| |/ / |/| | | | | | | | | | | | | | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
* | | Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ↵Gravatar Pierre-Marie Pédrot2018-06-14
|\ \ \ | | | | | | | | | | | | of submodules.
| | * | [vernac] Add option to force building really mutual induction schemesGravatar Matthieu Sozeau2018-06-13
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | Currently, if one of the inductives is non recursive, it defaults to a case analysis schems taking fewer predicates and methods just for that inductive. This irregularity prevents doing a combined scheme afterwards to gather all eliminators into one, as combined scheme expects all the eliminators to have the same predicates and methods. I have a use case in building function graphs in Equations where some of the inductives might not be recursive but I expect many other use cases could exist.
* | | [api] Add compatiblity Misctypes module.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | To be removed in 8.10.
* | | [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | We move the last 3 types to more adequate places.
* | | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | | | | - move_location to proofs/logic. - intro_pattern_naming to Namegen.
* | | [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | |
| | * Existing Class noop when already a class + warning.Gravatar Gaëtan Gilbert2018-06-08
| |/ |/| | | | | Fix #5012.
* | Merge PR #6874: [econstr] Some minor tweaksGravatar Pierre-Marie Pédrot2018-06-07
|\ \
* \ \ Merge PR #7453: Refuse to parse empty [Context] command.Gravatar Matthieu Sozeau2018-06-05
|\ \ \
* \ \ \ Merge PR #7315: An attempt to clarify error message for Arguments needing ↵Gravatar Maxime Dénès2018-06-04
|\ \ \ \ | | | | | | | | | | | | | | | "rename" flag
* \ \ \ \ Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \
| | | | * | [econstr] Remove some Unsafe.to_constr use.Gravatar Emilio Jesus Gallego Arias2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | Most of it seems straightforward.
| | | | * | [vernac] Switch back `auto_ind_decl` to Constr.Gravatar Emilio Jesus Gallego Arias2018-06-04
| |_|_|/ / |/| | | | | | | | | | | | | | AFAICT this tactic is always used on ground terms.
* | | | | Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7657: Fix a couple typos in deprecation messagesGravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \ \ \ \
| | | | | | | * | Refuse to parse empty [Context] command.Gravatar Gaëtan Gilbert2018-06-02
| |_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The error is now: Syntax error: [constr:binder] expected after 'Context' (in [vernac:gallina_ext]). Close #7452.
| * | | | | | | Fix a couple typos in deprecation messagesGravatar Armaël Guéneau2018-05-31
| | | | | | | |
| | | | | * | | Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Armaël Guéneau2018-05-31
| | |_|_|/ / / | |/| | | | |
* | | | | | | [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
* | | | | | | [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
|/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better.
* | | | | | Merge PR #6969: [api] Remove functions deprecated in 8.8Gravatar Maxime Dénès2018-05-31
|\ \ \ \ \ \
* | | | | | | Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Gaëtan Gilbert2018-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Close #7562. [api] move hint_info ast to tactics.
| * | | | | | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
|/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
* | | | | | Merge PR #7260: Fix #6951: Unexpected error during scheme creation.Gravatar Maxime Dénès2018-05-30
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\ \ \ \ \ \ \
| | | | * | | | Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Gaëtan Gilbert2018-05-30
| |_|_|/ / / / |/| | | | | |
| | * | | | | Fix #6951: Unexpected error during scheme creation.Gravatar Pierre-Marie Pédrot2018-05-29
| |/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | When creating a scheme for bifinite inductive types, we do not create a fixpoint.
* | | | | | Merge PR #7521: Fix soundness bug with VM/native and cofixpointsGravatar Pierre-Marie Pédrot2018-05-28
|\ \ \ \ \ \
| * | | | | | Unify pre_env and envGravatar Maxime Dénès2018-05-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We now have only two notions of environments in the kernel: env and safe_env.
| | * | | | | [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make the vernacular implementation self-contained in the `vernac/` directory. To this extent we relocate the parser, printer, and AST to the `vernac/` directory, and move a couple of hint-related types to `Hints`, where they do indeed belong. IMO this makes the code easier to understand, and provides a better modularity of the codebase as now all things under `tactics` have 0 knowledge about vernaculars. The vernacular extension machinery has also been moved to `vernac/`, this will help when #6171 [proof state cleanup] is completed along with a stronger typing for vernacular interpretation that can distinguish different types of effects vernacular commands can perform. This PR introduces some very minor source-level incompatibilities due to a different module layering [thus deprecating is not possible]. Impact should be relatively minor.
| | * | | | | [tactics] Turn boolean locality hint parameter into a named one.Gravatar Emilio Jesus Gallego Arias2018-05-27
| | | | | | |
| | * | | | | [api] [parsing] Move Egram* to `vernac/`Gravatar Emilio Jesus Gallego Arias2018-05-27
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The extension mechanism is specific to metasyntax and vernacinterp, thus it makes sense to place them next to each other. We also fix the META entry for the `grammar` camlp5 plugin.
* / / / / / Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
|/ / / / / | | | | | | | | | | | | | | | We address the easy ones, but they should probably be all removed.
| | | * / An attempt to clarify error message for Arguments needing "rename" flag.Gravatar Hugo Herbelin2018-05-25
| |_|/ / |/| | | | | | | | | | | | | | | Using a formulation which makes it is clear that no renaming has been done. See discussion at issue #2987.
* | | | Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵Gravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ \ | | | | | | | | | | | | | | | in CArray
| * | | | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
| | | | |
* | | | | [api] Move `Vernacexpr` to parsing.Gravatar Emilio Jesus Gallego Arias2018-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were a few spurious dependencies on the `Vernac` AST in the pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing, where they do belong more.
* | | | | [api] Move `opacity_flag` to `Proof_global`.Gravatar Emilio Jesus Gallego Arias2018-05-23
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | `Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed.
* | | | Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\ \ \ \
| | * | | Fix an anomaly when calling Obligation 0 or Obligation -1.Gravatar Théo Zimmermann2018-05-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I didn't change the parser which expects an integer instead of a positive number because changing it would also mean having worse error messages because of our current LL parser. The error message would have been: Syntax error: 'Tactic' ':=' expected after 'Obligation' (in [vernac:command]).
* | | | | [ide] Remove special option `-ideslave`Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | | | | | | | | | | | This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag.
* | | | | [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
* | | | Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\ \ \ \
| | * | | Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
| | | | |
| | * | | Remove unused argument to solve_constraints_systemGravatar Gaëtan Gilbert2018-05-17
| | | | |
| | * | | Move solve_constraint_system near its only use site (comInductive)Gravatar Gaëtan Gilbert2018-05-17
| | | | |
| | * | | Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 01:27:58 +0000