aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacinterp.ml
Commit message (Collapse)AuthorAge
...
* | | Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ↵Gravatar Maxime Dénès2017-06-05
|\ \ \ | | | | | | | | | | | | a flag suspectingly renamed in a clearer way
| | * | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* | | Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \
| | * | Renaming allow_patvar flag of intern_gen into pattern_mode.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | This highlights that this is a binary mode changing the interpretation of "?x" rather than additionally allowing patvar.
| | | * Factorizing interp_gen through a function interpreting glob_constr.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The new function is interp_glob_closure which is basically a renaming and generalization of interp_uconstr. Note a change of semantics that I could however not observe in practice. Formerly, interp_uconstr discarded ltac variables bound to names for interning, but interp_constr did not. Now, both discard them. We also export the new interp_glob_closure.
| | | * Splitting interp_open_constr into two variants, with or without type classes.Gravatar Hugo Herbelin2017-05-31
| | |/ | | | | | | | | | | | | | | | | | | This simplifies the API as before, inference of instances of type classes was iff a type constraint was given. We then export these both versions of interp_open_constr.
| * / Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| |/ | | | | | | | | | | | | | | | | | | | | | | This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
* | Adding "epose", "eset", "eremember" which allow to set terms withGravatar Hugo Herbelin2017-05-30
| | | | | | | | | | | | | | | | | | | | | | evars. This is for consistency with the rest of the language. For instance, "eremember" and "epose" are supposed to refer to terms occurring in the goal, hence not leaving evars, hence in general pointless. Eventually, I guess that "e" should be a modifier (see e.g. the discussion at #3872), or the difference is removed.
* | Adding "eassert", "eenough", "epose proof", which allow to stateGravatar Hugo Herbelin2017-05-30
|/ | | | a goal with unresolved evars.
* Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \ \
* \ \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \
| | * | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| | | * Clarifying the interpretation path for the "constr_with_binding" argument.Gravatar Hugo Herbelin2017-05-22
| | |/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility.
| | * Generalizing the tactic-in-term embedding to any generic argument.Gravatar Pierre-Marie Pédrot2017-05-03
| | |
| | * Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
| |/
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| |
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| |
* | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
| |
* | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes.
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | Now it is a private field, locations are optional.
* | [location] Use located in tactics.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | One case missing due the TACTIC EXTEND macro.
* | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
| |
* | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
| |
* | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/ | | | | | | | | This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location.
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| |
| * Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | We make apparent in the API that the implicit tactic is set or not. This was costing a lot in Pretyping for no useful reason, as it is almost always unset and the default implementation was just failing immediately.
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
|/ | | | | | All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component.
* Merge PR#428: Report missing tactic arguments in error messageGravatar Maxime Dénès2017-03-17
|\
* | Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
| | | | | | | | | | | | | | - Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390.
| * Report missing tactic arguments in error messageGravatar Tej Chajed2017-03-14
|/ | | | | | Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
* Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
|
* Merge PR#395: Allow hintdb to be parameters in a Ltac definition orGravatar Maxime Dénès2017-02-27
| | | | Tactic Notation
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 15:23:47 +0000