aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Collapse)AuthorAge
...
* | | 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
|\|
| * Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
| | | | | | | | | | while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion).
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2016-04-04
|\ \ | | | | | | | | | into JasonGross-trunk-function_scope
* | | Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
| | |
* | | Removing dead code in Genarg.Gravatar Pierre-Marie Pédrot2016-03-19
| | |
* | | Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there.
* | | Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
| | |
* | | Adopting the same rules for interpreting @, abbreviations andGravatar Hugo Herbelin2016-03-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | notations in patterns than in terms, wrt implicit arguments and scopes. See file Notations2.v for the conventions in use in terms. Somehow this could be put in 8.5 since it puts in agreement the interpretation of abbreviations and notations in "symmetric patterns" to what is done in terms (even though the interpretation rules for terms are a bit ad hoc). There is one exception: in terms, "(foo args) args'" deactivates the implicit arguments and scopes in args'. This is a bit complicated to implement in patterns so the syntax is not supported (and anyway, this convention is a bit questionable).
* | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
| | |
* | | A more explicit name to the asymmetric boolean flag.Gravatar Hugo Herbelin2016-03-12
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ | | |/ | |/|
| * | Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Gravatar Pierre-Marie Pédrot2016-03-03
| | | | | | | | | | | | | | | | | | | | | Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash.
* | | Printing notations: Cleaning in anticipation of fixing #4592.Gravatar Hugo Herbelin2016-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Making a clear distinction between expressions of the notation which are associated to binding variables only (as in `Notation "'lam' x , P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))') and those which are associated to at list one subterm (e.g. `Notation "x .+1" := (S x)' but also "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))' as in #4592). The former have type NtnTypeOnlyBinder. - Thus avoiding in particular encoding too early Anonymous as GHole and "Name id" as "GVar id". There is a non-trivial alpha-conversion work to do to get #4592 working. See comments in Notation_ops.add_env.
* | | The tactic generic argument now returns a value rather than a glob_expr.Gravatar Pierre-Marie Pédrot2016-02-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 03:39:45 +0000