aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Collapse)AuthorAge
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\
* | 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
* | Fixing #4865 (deciding on which arguments to recompute scopes was not robust).Gravatar Hugo Herbelin2016-06-29
| | | | | | | | See 4865.v for details.
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* | Properly handling the only printing flag when parsing rules already exist.Gravatar Pierre-Marie Pédrot2016-06-28
| |
| * Univs: allowing notations to take univ instancesGravatar Matthieu Sozeau2016-06-27
| | | | | | | | They can apply to the head reference under a notation.
| * Forbidding silently dropped universes instances inGravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | internalization. Patch by PMP, test-suite fix by MS.
* | Merge remote-tracking branch 'github/pr/223' into feedback-locationsGravatar Maxime Dénès2016-06-27
|\ \ | | | | | | | | | Was PR#223: Allow feedback messages to carry a location.
* | | minor: comment on the meaning of the 'boolean' variableGravatar Gabriel Scherer2016-06-27
| | |
* | | minor: documentation comment for constrintern.ml:sort_fieldsGravatar Gabriel Scherer2016-06-27
| | | | | | | | | | | | | | | (Because the function is private to the module, it is documented in the .ml rather than the .mli)
* | | minor: interp/constrintern.ml, clarify field completionGravatar Gabriel Scherer2016-06-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | The type of the user-defined function "completer" changes to be simpler and better reflect its purpose: provide values for missing field assignments. In the future we may want to also pass the name of the field as parameter (currently only the index is given, and both uses of the function ignore it), in particular if we want to implement { r with x = ...; y = ... }.
* | | minor: in constrintern.ml:sort_fields, clarify sfGravatar Gabriel Scherer2016-06-27
| | | | | | | | | | | | | | | The internal `add_pat` function is replaced by a call to `CList.extract_first`.
* | | minor: in constrintern.ml:sort_fields, clarify build_pattGravatar Gabriel Scherer2016-06-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The code was a big "try..with" defining all useful quantities at once. I tried to lift definitions out of this try..with to define them as early as possible: the record's information and the first field name are fetched before processing the other fields. There were two calls in the try..with body that could raise the Not_found exception (or at least I don't know the code well enough to be sure that either of them cannot): `shortest_qualid_of_global` and `build_patt`. They are now split in two separate try..with blocks, both raising the same exception (with a shared error message named `env_error_msg`). Someone familiar with the invariants at play could probably remove one of the two blocks, streamlining the code even further. I'm a bit surprised by the main logic part (the big (if .. else if .. else if ..) block in the new code), and there is a question in a comment. I hope to get it answered during code review and remove it (and maybe simplify the code). Finally, there was an apparently-stale comment in the code: (* insertion of Constextern.reference_global *) of course Constextern.reference_global corresponds to now function that I could find. After trying to understand the meaning of this comment, I decided to just remove it.
* | | whitespace: untabity constrinternl.ml:sort_fieldsGravatar Gabriel Scherer2016-06-27
| | |
* | | minor clarifications in constrintern.ml:sort_fieldsGravatar Gabriel Scherer2016-06-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that turning let boolean = not regular in if boolean && complete then ...; if boolean && complete then ...; into if not regular && complete then ...; if not regular && complete then ...; has absolutely no performance cost: negation inside a conditional is not computed as a boolean, it only flips the branches. The code is more readable because "boolean" was a terrible variable name.
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | | | | | | | | | Cf CHANGES for details.
| * | [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
|/ / | | | | | | | | | | | | | | This is a first step to relay location info in an uniform way, as needed by warnings and other mechanisms. The location info remains unused for now, but coqtop printing could take advantage of it if so wished.
* | Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Gravatar Hugo Herbelin2016-06-24
| |
* | Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq.
* | Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-06-16
| | | | | | | | implicit arguments when in beautification mode.
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-06-16
| | | | | | | | | | | | | | | | | | | | computing the arguments which allows to decide which list of implicit arguments to consider when several such lists are available. For instance, "eq_refl (A:=nat)" is now interpreted as "@eq_refl nat _", the same way as if we had said: Arguments eq_refl {A} {x}.
* | Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \ \ | | |/ | |/|
| * | Fix bug #4777: Printing time is impacted by large terms that don't print.Gravatar Pierre-Marie Pédrot2016-06-07
| | | | | | | | | | | | | | | We delay the externalization of application arguments in Constrextern, so that they only get computed when they are actually explicitly displayed.
| | * Removing the use to Egramcoq.recover_constr_grammar.Gravatar Pierre-Marie Pédrot2016-06-07
| |/ |/|
* | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | functions about interpretation, internalization, externalization of notations. Main syntactic changes: - subst_aconstr_in_glob_constr -> instantiate_notation_constr (because aconstr has been renamed to notation_constr long time ago) - extern_symbol -> extern_notation (because symbol.ml has been renamed to notation.ml long time ago) - documentation of notations_ops.mli Main semantic changes: - Notation_ops.eq_glob_constr which was partial eq disappears: use glob_constr_eq instead - In particular, this impacts a change on funind which now use the (fully implemented) glob_constr_eq Somehow, instantiate_notation_constr should be in notation_ops.ml for symmetry with match_notation_constr but it is bit painful to do.
* | Removing pointless field NPatVar. It does not make sense to have MetaGravatar Hugo Herbelin2016-06-02
| | | | | | | | and Evar in notations, and there are anyway already forbidden.
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
| |
* | Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Increase the size of the dumpglob buffer for cooking notations (bug #4708).Gravatar Guillaume Melquiond2016-05-04
| | | | | | | | A single terminal character can take up to 5 bytes, e.g. "''^A'".
| * Fix bug #3825: Universe annotations on notations should pass through or be ↵Gravatar Pierre-Marie Pédrot2016-05-03
| | | | | | | | rejected.
* | Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
* | Revert "Not taking arguments given by name or position into account when"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit f7ea0193c1aac918d8ed2df0d53df38dde5d1152.
* | Revert "Being defensive in printing implicit arguments also with manual"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 2211eeda012477b26081738fccc59aa31fb0a565.
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
* | Revert "Warn about possible shadowing of a name occurring in a "in" clause."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 46f876a9404844487476415af2e6f6d938558d15.
* | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | EXTEND and"" This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
* | Warn about possible shadowing of a name occurring in a "in" clause.Gravatar Hugo Herbelin2016-04-27
| |
* | Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
| | | | | | | | VERNAC EXTEND.
* | Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-04-27
| | | | | | | | implicit arguments when in beautification mode.
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | computing the arguments which allows to decide which list of implicit arguments to consider when several such lists are available.
* | A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Notation "## c" := (S c) (at level 0, c at level 100). which break the stratification of precedences. This works for the case of infix or suffix operators which occur in only one grammar rule, such as +, *, etc. This solves the "constr" part of #3709, even though this example is artificial. The fix is not complete. It puts extra parenthesese even when it is end of sentence, as in Notation "# c % d" := (c+d) (at level 3). Check fun x => # ## x % ## (x * 2). (* fun x : nat => # ## x % (## x * 2) *) The fix could be improved by not always using 100 for the printing level of "## c", but 100 only when not the end of the sentence. The fix does not solve the general problem with symbols occurring in more than one rule, as e.g. in: Notation "# c % d" := (c+d) (at level 1). Notation "## c" := (S c) (at level 0, c at level 5). Check fun x => # ## x % 0. (* Parentheses are necessary only if "0 % 0" is also parsable *) I don't see in this case what better approach to follow than restarting the parser to check reversibility of the printing.
* | Fixing a "This clause is redundant" error when interpreting the "in"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | clause of a "match" over an irrefutable pattern.
* | Reformatting + removal of some useless data + some cut-eliminationGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | in interning of patterns. No semantic changes (except the type of ids_of_cases_indtype).
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 18:58:50 +0000