aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Collapse)Author
2020-02-20Merge PR #11143: In Print/Check/Show, adopt the view that the attached type ↵Emilio Jesus Gallego Arias
information may impact the display of coercion and implicit arguments. Reviewed-by: ejgallego
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding ↵Emilio Jesus Gallego Arias
notation format + new notion of format associated to a given interpretation Ack-by: maximedenes
2020-02-20Unconditionally print explanation for universe inconsistenciesGaëtan Gilbert
ie regardless of the Print Universes flag. AFAICT there is no point in skipping them.
2020-02-19Merge PR #11636: Revert buggy commit mistakenly pushed with #11530Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ↵Hugo Herbelin
entries)." This reverts commit 29919b725262dca76708192bde65ce82860747be. It was pushed by mistake as part of #11530. Sorry about it.
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
We do two changes: - We distinguish between a notion of format generically attached to notations and a new notion of format attached to interpreted notations. "Reserved Notation" attaches a format generically. "Notation" attaches the format specifically to the given interpretation, and additionally, attaches it generically if it is the first time the notation is defined. - We warn before overriding an explicitly reserved generic format, or a specific format.
2020-02-19Only parsing in Reserved Notation: turning notice into a warning.Hugo Herbelin
2020-02-19ComInductive: use lbound=Prop iff non polymorphicGaëtan Gilbert
This avoids having to interp params and intern arities twice.
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
to control uniform parameters. This replaces the attribute.
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
This reverts commit 03c48bb6943312e606b80b7af65b1ccb7122a386.
2020-02-16Suite picking numeral notationHugo Herbelin
Ceci est une suite à numeral notation in custom entries, cherchant à raffiner la compatibilité entre entrées. C'est mélangé avec le "pick" précédent, et c'est en chantier.
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-16Fixing bug #9521 (anomaly due to missing declaration of level in custom entry).Hugo Herbelin
This fixes also #9640 part 1.
2020-02-16Mini-factorization in vernac grammar.Hugo Herbelin
Unfortunately, we cannot factorize further | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind | x = IDENT; b = constr_as_binder_kind without losing the rule | x = IDENT; typ = syntax_extension_type
2020-02-16Custom entries: accept that no level is mentioned for a subentry.Hugo Herbelin
If it is for an internal non-terminal then: - if for a subentry different from constr, it refers to the head of the subentry - if in constr, it is 200 by convention If it is on the border of a rule, then: - if it is in a subentry different from the entry it lives, it refers to the head of the subentry (or 200 by convention if in constr) - if it is in the same entry, the rule for associativity tells if a SELF, a NEXT, or (if on the right) a LEVEL
2020-02-15Reusing type production_level for the result of adjust_level.Hugo Herbelin
2020-02-15Reorganize type "production_level" along a more intuitive structure.Hugo Herbelin
NextLevel = at next level NumLevel n = at level n DefaultLevel = <no mention of level>
2020-02-15Dead code in Egramcoq.adjust_level.Hugo Herbelin
2020-02-15Fixing a precedence printing bug with custom entries.Hugo Herbelin
Insertion of coercion to manage precedence of custom entries are treated in constrextern.ml, while ppconstr.ml is only about the management of precedences for constr.
2020-02-15Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
There was a collision at the time of interpreting subentries (in metasyntax.ml) but also at the time of "optimizing" the entries (in egramcoq.ml). Also fixes #9517, fixes #9519, fixes #9640 (part 3).
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
2020-02-13Delete unused commentGaëtan Gilbert
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2020-02-13Merge PR #11407: [mltop] Store digest of modules used to compile files.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: maximedenes
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-13Merge PR #11424: Check instance length in type_of_{inductive,constructor}Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
The standard use is to repeat the option keywords in lowercase, which is basically useless. En passant add doc entry for Dump Arith.
2020-02-12Check instance length in type_of_{inductive,constructor}Gaëtan Gilbert
2020-02-12ReferenceVariables error contains a globref instead of a constrGaëtan Gilbert
The previous system was from before globref was in the kernel.
2020-02-12Merge PR #11546: Remove the Template Check option.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-02-11Fixing some residual bugs of PR #10202 (manual implicit args in subterms).Hugo Herbelin
- Implicit arguments in the return clause and in the branches of a match were not checked. - Implicit arguments in each declaration of intern_context were not restarted. - Additionally, in intern_context, we take into account ids from the env on top of which intern_context is called. - A better approximation of the check for manual implicit in notations improved (though not fully correct because the exact context of interpretation of a binder in a notation with recursive binders is not known). We also rename impl_binder_index into binder_block_names in anticipation of checking redundancies also for non-implicit arguments.
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: maximedenes
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2020-02-06unsafe_type_of -> type_of in ComCoercion.build_id_coercionGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Auto_ind_decl.do_replace_blGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in ComProgramFixpoint.build_wellfoundedGaëtan Gilbert
We typecheck it literally the previous line...
2020-02-06Merge PR #11478: Nicer kernel universe error for inductivesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-06Merge PR #10835: Accepting a few more variants of format for recursive ↵Pierre-Marie Pédrot
notations (+ a fix about locations) Reviewed-by: ppedrot
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-01-31More tolerant in format for recursive notations.Hugo Herbelin
This is probably a bit overkill but users are tempted to experiment it, so we accept that both ends of a recursive notation are surrounded with boxes which contain printing hints. The alternative would have been to forbid the ends of a recursive notation to be in boxes, but strictly speaking it is a bit more restricting, even if I don't see a realistic use of the general form.
2020-01-30[exn] Don't reraise in exception printersEmilio Jesus Gallego Arias
This behaviour seems a bit dubious and it is indeed not needed, also such re-raises seem like they will mess with the backtrace.
2020-01-30Notations: Fixing a wrong location in format.Hugo Herbelin
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
Reviewed-by: maximedenes
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
This seems seldom used and I think in general instrumentation this way is pretty limited (usually better to use the build system to tweak) It thus seems worth removing as to simplify `Mltop` a bit, but of course comments are welcome.
2020-01-29Nicer kernel universe error for inductivesGaëtan Gilbert
Not sure if it's possible to see it without a plugin.
2020-01-29Merge PR #11408: [mltop] Remove error handling hacks in favor of default ↵Pierre-Marie Pédrot
methods. Reviewed-by: ppedrot
2020-01-28Remove dead code in Globnames.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 19:11:31 +0000