Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix #7421: constr_eq ignores universe constraints. | Gaëtan Gilbert | 2018-06-18 |
| | | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong. | ||
* | Fix #7615: Functor inlining drops universe substitution. | Pierre-Marie Pédrot | 2018-06-07 |
| | | | | | | | We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case. | ||
* | Make direct invocations of `simple apply` obey `Opaque` directive. | Maxime Dénès | 2018-06-05 |
| | | | | | When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues. | ||
* | Merge PR #7229: Deprecate implicit tactic solving. | Hugo Herbelin | 2018-06-04 |
|\ | |||
* \ | Merge PR #7486: Update old parts of CHANGES to use current bug numbers. | Hugo Herbelin | 2018-06-04 |
|\ \ | |||
| | * | Documenting the deprecation. | Pierre-Marie Pédrot | 2018-06-04 |
| |/ |/| | |||
* | | Add CHANGES entry | Maxime Dénès | 2018-05-28 |
| | | |||
* | | [tactics] Remove anonymous fix/cofix form. | Emilio Jesus Gallego Arias | 2018-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. | ||
* | | [stm] Make toplevels standalone executables. | Emilio Jesus Gallego Arias | 2018-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. | ||
* | | Document nested proofs and associated option. | Théo Zimmermann | 2018-05-17 |
| | | |||
| * | Update old parts of CHANGES to use current bug numbers. | Théo Zimmermann | 2018-05-11 |
| | | |||
* | | Notations: advertize that distinct "only parsing"/"only printing" rules work. | Hugo Herbelin | 2018-05-11 |
|/ | |||
* | Make "intro"/"intros" progress on existential variables. | Hugo Herbelin | 2018-05-02 |
| | |||
* | Strict focusing using Default Goal Selector. | Gaëtan Gilbert | 2018-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. | ||
* | Merge PR #7244: Making tactic-in-term aware of "Set Ltac Debug" | Pierre-Marie Pédrot | 2018-04-23 |
|\ | |||
* | | Fix typo in CHANGES. | Maxime Dénès | 2018-04-16 |
| | | |||
* | | Mention other deprecations and fixes in CHANGES | Maxime Dénès | 2018-04-16 |
| | | |||
* | | CHANGES: document COQFLAGS change | Ralf Jung | 2018-04-16 |
| | | |||
* | | Merge PR #7200: [ltac] Deprecate nameless fix/cofix. | Maxime Dénès | 2018-04-16 |
|\ \ | |||
* | | | Add missing CHANGES entry for #6169. | Théo Zimmermann | 2018-04-14 |
| | | | | | | | | | | | | Fixes #7243. | ||
| | * | Making tactic-in-term aware of "Set Ltac Debug". | Hugo Herbelin | 2018-04-13 |
| |/ |/| | |||
| * | [ltac] Deprecate nameless fix/cofix. | Emilio Jesus Gallego Arias | 2018-04-13 |
|/ | | | | | | | | | | | | LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171. | ||
* | Merge PR #7103: Fix #7101: STM delegation policy broken | Enrico Tassi | 2018-04-09 |
|\ | | | | | | | | | # Conflicts: # CHANGES | ||
* | | Fix #6404 - Print tactics called by ML tactics | Jason Gross | 2018-04-02 |
| | | |||
* | | Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092) | Pierre-Marie Pédrot | 2018-04-01 |
|\ \ | |||
* | | | Add CHANGES for removing Implicit Arguments and Arguments Scope | Jasper Hugunin | 2018-03-30 |
| | | | |||
| * | | Supporting fix/cofix in Ltac pattern-matching (wish #7092). | Hugo Herbelin | 2018-03-28 |
|/ / | | | | | | | | | This is done by not failing for fix/cofix while translating from glob_constr to constr_pattern. | ||
| * | Fix #7101: STM delegation policy broken | Maxime Dénès | 2018-03-28 |
|/ | | | | | I make here a minimal fix, but a lot of cleaning should be done around Aux_file handling, including removing some code from the kernel. | ||
* | Merge PR #7018: Fix typo in CHANGES. | Maxime Dénès | 2018-03-23 |
|\ | |||
* | | update CHANGES | Enrico Tassi | 2018-03-23 |
| | | |||
| * | Fix typo in CHANGES. | Théo Zimmermann | 2018-03-19 |
|/ | | | | [skip ci] | ||
* | Add some missing entries in CHANGES | Maxime Dénès | 2018-03-15 |
| | |||
* | [doc] Document removal of deprecated options. | Emilio Jesus Gallego Arias | 2018-03-09 |
| | |||
* | Merge PR #6949: Revert PR #873: New strategy based on open scopes for ↵ | Maxime Dénès | 2018-03-09 |
|\ | | | | | | | deciding… | ||
* \ | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | 2018-03-09 |
|\ \ | |||
| | * | Revert "Merge PR #873: New strategy based on open scopes for deciding which ↵ | Maxime Dénès | 2018-03-09 |
| | | | | | | | | | | | | | | | | | | | | | notation to use among several of them" This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing changes made to 2f679ec5235257c9fd106c26c15049e04523a307. | ||
* | | | Merge PR #6923: Export options | Maxime Dénès | 2018-03-09 |
|\ \ \ | |_|/ |/| | | |||
| | * | Documentation for Cumulativity Weak Constraints. | Gaëtan Gilbert | 2018-03-09 |
| | | | |||
* | | | Merge PR #6480: Allow Prop as source for coercions | Maxime Dénès | 2018-03-09 |
|\ \ \ | |_|/ |/| | | |||
* | | | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès | 2018-03-09 |
|\ \ \ | |||
| | | * | Documenting the Export modifier for options in CHANGES. | Pierre-Marie Pédrot | 2018-03-09 |
| |_|/ |/| | | |||
| | * | doc and changes for coercion from prop/type | charguer | 2018-03-09 |
| |/ |/| | |||
* | | Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵ | Maxime Dénès | 2018-03-09 |
|\ \ | | | | | | | | | | fiat-crypto/OSX | ||
* \ \ | Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵ | Maxime Dénès | 2018-03-08 |
|\ \ \ | | | | | | | | | | | | | wish #4129) | ||
* \ \ \ | Merge PR #6743: Add notation {x & P} for sigT | Maxime Dénès | 2018-03-08 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6909: Deprecate Focus and Unfocus | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6582: Mangle auto-generated names | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ \ | |||
* | | | | | | | [vernac] Warn when using “Require” in a section | Vincent Laporte | 2018-03-07 |
| | | | | | | | |||
* | | | | | | | Merge PR #6744: Add String.concat | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ | |||
| | | | | | * | | Add CHANGES and man entry for coqdep learning _CoqProject. | Gaëtan Gilbert | 2018-03-06 |
| | | | | | | | |