aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.ml
Commit message (Collapse)AuthorAge
...
* | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We get rid of a complex function doing both an incremental comparison and an effect on names (Notation_ops.compare_glob_constr). For the effect on names, it was actually already done at the time of turning glob_constr to notation_constr, so it could be skipped here. For the comparison, we rely on a new incremental variant of Glob_ops.glob_eq_constr (thanks to Gaëtan for getting rid of the artificial recursivity in mk_glob_constr_eq). Seizing the opportunity to get rid of catch-all clauses in pattern-matching (as advocated by Maxime). Also make indentation closer to the one of other functions.
* | | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
|/ / | | | | | | | | | | This was preventing to work examples such as: Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
* | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | |
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
| | |
* | | [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] Move Glob_term.predicate_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | We continue the uniformization pass. No big news here, trying to be minimally invasive.
* | | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/ / | | | | | | | | We continue the uniformization pass. No big news here, trying to be minimally invasive.
| * Better support for printing constructors with let-ins.Gravatar Hugo Herbelin2017-04-07
| | | | | | | | | | | | | | | | This allows e.g. to use the record notations even when there are defined fields. A priori fixed also missing parameters when interpreting primitive tokens.
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\ \
| * | 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.
| * | Using the same type of binders for interning and externing.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | Previously a union type was used for externing. In particular, moving extended_glob_local_binder to glob_constr.ml.
* | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
|/ / | | | | | | | | | | Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-29
| |\
| | * Fixing #5161 (case of a notation with unability to detect a recursive binder).Gravatar Hugo Herbelin2016-10-27
| | | | | | | | | | | | | | | Type annotations in unrelated binders were badly interfering with detection of recursive binders in notations.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| |
| * | Quick fix to #4595 (making notations containing "ltac:" unused for printing).Gravatar Hugo Herbelin2016-10-04
| | | | | | | | | | | | Also getting rid of a global side-effect.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| |
| * | Warning about similar notations now up to alpha-conversion.Gravatar Hugo Herbelin2016-09-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to define on purpose the very same notation in different files, as currently the notations for *, +, - in Nat.v and Peano.v (with the first one using variables n and m and the second one using the default variables used by Infix, namely x and y). This makes also the "notation-overridden" warning less enigmatic facing two notations which are the same up to the choice of names.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| |
* | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | I hadn't realized that this PR uses OCaml's 4.03 inlined records feature. I will advocate again for a switch to the latest OCaml stable version, but meanwhile, let's revert. Sorry for the noise. This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
* | | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | The new name makes it more obvious what is meant here by "kind". We leave Decl_kinds.binding_kind as a deprecated alias for plugin compatibility. We also replace bool with implicit_status in a few places in the codebase.
| * | Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
| | | | | | | | | | | | One of them revealed a true bug.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\| |
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
| |\|
| | * Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Gravatar Hugo Herbelin2016-09-12
| | |
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \ | |/ / |/| |
* | | Notation_ops.subst_glob_vars: substituting also in evar kind forGravatar Hugo Herbelin2016-09-01
| | | | | | | | | | | | consistency of the use of names.
* | | Fix bug #4764: Syntactic notation externalization breaks.Gravatar Pierre-Marie Pédrot2016-08-28
| | |
| * | 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.
| * | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
* | Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
| |
* | Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | | | | | | | | | | | - typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me.
* | Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | Supporting accordingly printing of sequences of binders including binding patterns.
* | Notations with multiple recursive binders: fixing use of alpha-conversion.Gravatar Hugo Herbelin2016-07-19
| |
* | Notations: fixing multiple binders used as terms in reverse order.Gravatar Hugo Herbelin2016-07-19
| |
* | Removing a source of clash with multiple recursive patterns in notations.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | | | | | | | | | | | | | The same variable name was used to collect the binders and the successive steps of matching one binder, resulting in unexpected attempts for merging in the presence of multiple occurrence of the same recursive pattern. An amusing side-effect: when eta-expanding for a notation with recursive binders, it is the second variable of the "x .. y" which is used to invent a name rather than the first one.
* | A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
| | | | | | | | | | | | | | A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns).
* | Partial fix to #4592 (notation requiring alpha-conversion for printing).Gravatar Hugo Herbelin2016-07-17
| |
* | Fixing a bug in recognizing a recursive pattern of notationsGravatar Hugo Herbelin2016-07-17
| | | | | | | | immediately in the scope of another recursive pattern.
* | Fixing interpretation of notations w/ opposite instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17
| |
* | Fixing printing of notations with several instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17
| |
* | First step in adding printing for notations such as given in #4932.Gravatar Hugo Herbelin2016-07-17
| | | | | | | | | | | | | | | | In particular, it becomes possible to have recursive patterns used shared by binders and terms. Currently limited by alpha-conversion issues (e.g. test2 from 4932.v is not reprinted).
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | | | | | Cf CHANGES for details.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 15:57:50 +0000