aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
Commit message (Collapse)AuthorAge
...
* | [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] 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 PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\
* | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | | | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
| * Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| |\ | |/ |/|
| * Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| |\
* | | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.
* | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
|\ \
* | | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | | | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
| * | [cleanup] Change Id.t option to Name.t in TacFunGravatar Tej Chajed2017-02-16
|/ /
| * Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
| |\ | |/ |/|
| * Porting the ssrmatching plugin to the new EConstr API.Gravatar Enrico Tassi2017-02-14
| |
| * Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
| * Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
| |
| * Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \
| * | ssrmatching: fix iter_constr_LR iterator wrt ProjGravatar Enrico Tassi2016-12-07
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\| |
| * | ssrmatching: handle primite projections (fix: #5247)Gravatar Enrico Tassi2016-12-05
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\| | | |/ |/|
| * Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ | | | | | | | | | Was PR#331: Solve_constraints and Set Use Unification Heuristics
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| |
| * | Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ | | | | | | | | | | | | Was PR#319: More error tagging, try to fix bug 5135
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | |
| * | | ssrmatching: fix interpretation of rpatternGravatar Enrico Tassi2016-10-24
| | | |
| | | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | |/ | |/| | | | | | | | | | reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
| | * [pp] Use more convenient pp API in ssrmatchingGravatar Emilio Jesus Gallego Arias2016-10-18
| | |
| | * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |/ | | | | | | | | | | | | | | The current tag system in `Pp` is generic, which implies we must choose a tagging function when calling a printer. For console printing there is a single choice, thus this commits adds it a few missing cases.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
* | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| | | | | | | | | | | | There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
| * Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
| | | | | | | | One of them revealed a true bug.
* | Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-15
| |
* | Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
| |
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | Suggested by @ppedrot
* | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 11:21:40 +0000