aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\
* \ Merge PR #7888: Clarify the message "this hint will only be used by eauto"Gravatar Pierre-Marie Pédrot2018-06-27
|\ \
* \ \ Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeftGravatar Hugo Herbelin2018-06-26
|\ \ \
| | | * Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |_|/ |/| |
| | * Clarify the message "this hint will only be used by eauto"Gravatar Armaël Guéneau2018-06-25
| |/ |/|
* | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | This brings more compatibility with handling of mutual primitive records in the kernel.
* | Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\ \
* | | Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
| | | | | | | | | | | | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
| * | 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.
| * evd: restrict_evar with candidates, can raise NoCandidatesLeftGravatar Matthieu Sozeau2018-06-15
|/ | | | | | | | | | | | | | | | | | When restricting an evar with candidates, raise an exception if this restriction would leave the evar without candidates, i.e. unsolvable. - evarutil: mark restricted evars as "cleared" They would otherwise escape being catched by the [advance] function of clenv, and result in dangling evars not being registered to the shelf. - engine: restrict_evar marks it cleared, update the future goals We make the new evar a future goal and remove the old one. If we did nothing, [unshelve tac] would work correctly as it uses [Proofview.advance] to find the shelved goals, going through the cleared evar. But [Unshelve] would fail as it expects only undefined evars on the shelf and throws away the defined ones.
* Merge PR #7789: Fixes #7779: destruct's "in" clause was forgetting the ↵Gravatar Pierre-Marie Pédrot2018-06-13
|\ | | | | | | possibility of an "eqn" clause
| * Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Gravatar Hugo Herbelin2018-06-12
| | | | | | | | | | | | | | | | This is a quick fix. Code should be made nicer along these lines: - try to pass the name of the variable created by "mkletin_goal" in the monad using "refine_one"; - use a disjunctive type of "inhyps" to indicate when it is meaningful, rather than using [].
* | [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | We move the last 3 types to more adequate places.
* | [api] Misctypes removal: tactic flags.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | We move the "flag types" to its use place, and mark some arguments with named parameters better.
* | [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: multi to tactics/rewriteGravatar Emilio Jesus Gallego Arias2018-06-12
|/
* Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is providedGravatar Matthieu Sozeau2018-06-07
|\
* \ Merge PR #6874: [econstr] Some minor tweaksGravatar Pierre-Marie Pédrot2018-06-07
|\ \
* \ \ Merge PR #7004: Make `simple apply` obey `Opaque` directive.Gravatar Pierre-Marie Pédrot2018-06-05
|\ \ \
* \ \ \ Merge PR #7099: Stronger invariants in unification signature.Gravatar Matthieu Sozeau2018-06-05
|\ \ \ \
| | * | | 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 #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.
| | * | Stronger invariants in unification signature.Gravatar Pierre-Marie Pédrot2018-06-04
| |/ / |/| | | | | | | | | | | | | | | | | We use an option type instead of returning a pair with a boolean. Indeed, the boolean being true was always indicating that the returned value was unchanged. The previous API was somewhat error-prone, and I don't understand why it was designed this way in the first place.
* | | Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Gravatar Matthieu Sozeau2018-06-04
|\ \ \
* \ \ \ Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ↵Gravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ | | | | | | | | | | | | | | | of List
* \ \ \ \ Merge PR #7640: Small refactoring to clarify make_local_hint_db.Gravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7649: Remove some dead code in class_tactics.mlGravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7637: Fix an outdated comment refering to lib/dnet.mliGravatar Pierre-Marie Pédrot2018-06-03
|\ \ \ \ \ \ \
| | | | * | | | Cleaning, documentation, uniformisation of the Coq extension of List.Gravatar Hugo Herbelin2018-06-03
| |_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Still some discrepancies though. E.g.: - some functions taking an equality as arguments have suffix `_f` but not all; - the functions possibly raising an error have still different kinds of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange, and when in the first two cases, with no unique rules in the style of the associated string - we thus avoid to document the exact string used). There are a few semantics changes: - skipn_at_least now raises a `Failure` if its argument is negative; - map3 raises an Invalid_argument "List.map3" rather than Invalid_argument "map3" and similarly for map4 - internally, map3 and map4 are now tail-recursive (by uniformity); - internally, split3 and combine3 are now tail-recursive (by uniformity); - filter is now "smart" by default and smartfilter is deprecated; - smartmap is now tail-recursive by default.
* | | | | | | Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\ \ \ \ \ \ \
| | | * | | | | Remove some dead code in class_tactics.mlGravatar Armaël Guéneau2018-05-31
| |_|/ / / / / |/| | | | | |
| | | | | * | Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Armaël Guéneau2018-05-31
| |_|_|_|/ / |/| | | | |
* | | | | | Merge PR #6969: [api] Remove functions deprecated in 8.8Gravatar Maxime Dénès2018-05-31
|\ \ \ \ \ \
| | * | | | | 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.
* | | | | | | 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 #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\ \ \ \ \
| | | * | | Small refactoring to clarify make_local_hint_db.Gravatar Théo Zimmermann2018-05-30
| | | | | |
| | * | | | Fix an outdated comment refering to lib/dnet.mliGravatar Armaël Guéneau2018-05-30
| | |/ / /
| | | | * Fix anomaly in autoapply when an unbound hint name is providedGravatar Armaël Guéneau2018-05-29
| | | |/ | | |/|
* | / | 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.
| * | [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
| | |
* | | 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.
* | 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
| |
* | Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
| |