aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Workaround to handle non-value arguments in tactics.Gravatar Cyprien Mangin2018-06-14
| | | | | Although the fix is not a proper one, it seems to solve every instance of #2800 that could be tested.
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | We move the last 3 types to more adequate places.
* [api] Misctypes removal: move Tactypes to proofsGravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | This gets `Tactypes` closer to `tactics/`, however some legacy stuff blocks it in `proofs`. We consider that is satisfactory for now.
* [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
|
* [api] Misctypes removal: multi to tactics/rewriteGravatar Emilio Jesus Gallego Arias2018-06-12
|
* Micromega clean-upGravatar Maxime Dénès2018-06-07
| | | | | | | | | We add .mli files, removed dead code and use standard combinators instead of redefined ad-hoc ones in a few places. A lot of cleaning still has to be done on this code: documenting the interfaces, resolving the many abstraction leaks. I suspect there is still a lot of code duplication.
* Make direct invocations of `simple apply` obey `Opaque` directive.Gravatar Maxime Dénès2018-06-05
| | | | | When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues.
* Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\
* \ Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Pierre-Marie Pédrot2018-06-04
|\ \
* \ \ Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Gravatar Matthieu Sozeau2018-06-04
|\ \ \
| | | * Deprecate implicit tactic solving.Gravatar Pierre-Marie Pédrot2018-06-04
| |_|/ |/| |
* | | Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\ \ \
| | | * 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.
| * | Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
| | | | | | | | | | | | | | | Instead of having the projection data in the constant data we have it independently in the environment.
* | | [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 #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\ \
* \ \ Merge PR #7621: Tactics.introduction: remove dangerous option ~checkGravatar Pierre-Marie Pédrot2018-05-30
|\ \ \
* \ \ \ Merge PR #7521: Fix soundness bug with VM/native and cofixpointsGravatar Pierre-Marie Pédrot2018-05-28
|\ \ \ \
| | * | | Tactics.introduction: remove dangerous option ~checkGravatar Enrico Tassi2018-05-28
| |/ / / |/| | | | | | | | | | | | | | | In locally nameless mode (proof mode) names in the context *must* be distinct otherwise the term representation makes no sense.
| * | | 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.
* | | | Merge PR #7419: Remove 100 occurrences of Evd.emptyGravatar Pierre-Marie Pédrot2018-05-28
|\ \ \ \ | |/ / / |/| | |
| | * | [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
| |/ / |/| |
* | | Merge pull request #7569 from ppedrot/clean-newringGravatar Assia Mahboubi2018-05-25
|\ \ \ | | | | | | | | Simplify the newring hack
* \ \ \ Merge PR #7524: [ssr] fix after to_constr ~abort_on_undefined_evars was addedGravatar Maxime Dénès2018-05-25
|\ \ \ \
| | | * | Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
| |_|/ / |/| | | | | | | | | | | We address the easy ones, but they should probably be all removed.
* | | | [tactics] Remove anonymous fix/cofix form.Gravatar Emilio Jesus Gallego Arias2018-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove the `fix N / cofix N` forms from the tactic language. This way, these tactics don't depend anymore on the proof context, in particular on the proof name, which seems like a fragile practice. Apart from the concerns wrt maintenability of proof scripts, this also helps making the "proof state" functional; as we don't have to propagate the proof name to the tactic layer.
* | | | Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵Gravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ \ | | | | | | | | | | | | | | | in CArray
| * | | | Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
| | | | |
| * | | | Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
| | | | |
| * | | | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
| | | | |
* | | | | [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.
| | * | Simplify the newring hack.Gravatar Pierre-Marie Pédrot2018-05-21
| | | | | | | | | | | | | | | | | | | | | | | | The new implementation is 100% compatible with the previous one, but it is more compact and does not use a tricky translation function from the kernel.
* | | | Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
| |/ / |/| |
* | | Merge PR #7359: Reduce usage of evar_map referencesGravatar Pierre-Marie Pédrot2018-05-17
|\ \ \
| | * | [ssr] fix after to_constr ~abort_on_undefined_evars was addedGravatar Enrico Tassi2018-05-16
| |/ / |/| |
* | | Merge PR #7213: Do not compute constr matching context if not used.Gravatar Matthieu Sozeau2018-05-15
|\ \ \
| | * | Deprecate Typing.e_* functionsGravatar Gaëtan Gilbert2018-05-14
| | | |
| | * | Deprecate Refiner [evar_map ref] exported functions.Gravatar Gaëtan Gilbert2018-05-14
| | | | | | | | | | | | | | | | Uses internal to Refiner remain.
| | * | Deprecate Evarconv.e_conv,e_cumulGravatar Gaëtan Gilbert2018-05-11
| | | |
| | * | Convert clear_hyps_in_evi to state passing style.Gravatar Gaëtan Gilbert2018-05-11
| | | |
| | * | Deprecate most evarutil evdref functionsGravatar Gaëtan Gilbert2018-05-11
| |/ / |/| | | | | | | | clear_hyps remain with no alternative
* | | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
* | | Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Pierre-Marie Pédrot2018-05-04
|\ \ \
* | | | [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select`
* | | | Merge PR #6935: Separate universe minimization and evar normalization functionsGravatar Pierre-Marie Pédrot2018-04-30
|\ \ \ \
* | | | | Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-07 22:15:04 +0000