aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-24[exn] Generate an anomaly if the exn printer raises.Emilio Jesus Gallego Arias
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
Raising inside exception printers is quite tricky as the order of registration for printers will indeed depend on the linking order. We thus forbid this, and make our API closer to the upstream `Printexn` by having printers return an option type.
2020-02-24Merge PR #11653: Tactic_matching.pattern_match_term: remove ignored ↵Pierre-Marie Pédrot
"refresh" argument Reviewed-by: ppedrot
2020-02-24Merge PR #11623: Deprecate unsafe_type_ofPierre-Marie Pédrot
Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-02-24Merge PR #11588: test for x[i] notation not breaking Ltac parsingGaëtan Gilbert
Reviewed-by: tchajed
2020-02-23Merge PR #11660: Fix #11654: syntax of inductive declaration.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-23Merge PR #11120: Refactoring code for application printing + fixing #11091 ↵Emilio Jesus Gallego Arias
(inconsistencies in parsing/printing notations to partial applications) Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: jfehrle
2020-02-23Merge PR #11637: Update copyright in refman to year 2020.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-02-23Merge pull request #11629 from ppedrot/fix-11552Tej Chajed
Fix #11552: Ltac2 breaks query commands during proofs.
2020-02-23Fix #11654: syntax of inductive declaration.Théo Zimmermann
Inductive foo := Bar |. was accepted but it shouldn't have.
2020-02-23Documenting inheritance of implicit arguments and scopes in notations.Hugo Herbelin
2020-02-23Addressing a changelog comment from Théo Zimmermann.Hugo Herbelin
2020-02-23Update ↵Hugo Herbelin
doc/changelog/03-notations/11120-master+refactoring-application-printing.rst Thanks Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-02-23Apply and generalize suggestions from Théo.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-02-22Merge PR #11651: [merge-script] Improve warning in case of batch merging.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-22Adding a changelog item.Hugo Herbelin
2020-02-22Fixes #4690: do not allow @f in notations when f is a notation variable.Hugo Herbelin
2020-02-22New parsing/printing pattern/terms imp/scopes tests summarizing last changes.Hugo Herbelin
2020-02-22Inherit arguments scopes in pattern notations bound to some @id.Hugo Herbelin
2020-02-22In printing patterns, distinguish the case of a notation to @id.Hugo Herbelin
This is a case which conventionally deactivates implicit arguments.
2020-02-22Inherit scopes and implicit sign. in notations for partially applied pattern.Hugo Herbelin
Exception: when the notation is to some @id. Formerly, this was ignored for all kinds of string notations.
2020-02-22Fix index bug in computing implicit signature of abbrev. in pattern printing.Hugo Herbelin
2020-02-22Fix inheritance of argument scopes when printing notations in patterns.Hugo Herbelin
2020-02-22Use auxiliary function for externing record patterns.Hugo Herbelin
Also apply the same conditions for printing constructors as record instances in both terms and patterns.
2020-02-22Inherit argument scopes in notations to expressions of the form @f.Hugo Herbelin
This is a change of semantics.
2020-02-22Propagate implicit arguments in all notations for partial applications.Hugo Herbelin
This was done for abbreviations but not string notations. This adopts the policy proposed in #11091 to make parsing and printing consistent.
2020-02-22Deactivate implicit arguments in printing notations bound to "@f".Hugo Herbelin
This is to match the parsing policy (see #11091). In particular, we deactivate also argument scopes, consistently with what is done at parsing time.
2020-02-22Fixing printing of notations bound to an expression of the form "@f".Hugo Herbelin
The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[]) encoding of @f was lost. It remains to let printing match parsing wrt the deactivation of implicit arguments and argument scopes in such case. See next commit.
2020-02-22Fixing a notation printing bug (missing a @ to reflect absence of imp. args).Hugo Herbelin
When a non-applied reference was matching a notation to the same reference, implicit arguments were lost.
2020-02-22Fixing anomaly from #11091 (incompatible printing with notation and imp. args).Hugo Herbelin
We fix also an index error in deciding when to explicit print a non-inferable implicit argument.
2020-02-22Merge PR #11596: ComInductive: use lbound=Prop iff non polymorphicEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-22Merge PR #11639: Fixes #10917: anomaly in building return clause of n-ary ↵Emilio Jesus Gallego Arias
pattern-matching problem Reviewed-by: ejgallego
2020-02-22Merge PR #11638: Add debugger printer for type GlobEnv.tEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-22Fixing a bug introduced in PR #10832 (new format specific to a given notation).Hugo Herbelin
The import of the format should not be done if i<>1 in open_notation.
2020-02-22Simplification of type unparsing (index of variable in UnpMetaVar is unused).Hugo Herbelin
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
Also renamed it to relative_entry_level. Correspondence between old and new representation is: (n,L) -> LevelLt n (n,E), (n,Prec n) -> LevelLe n (n,Any) -> LevelSome (n,Prec p) when n<>p was unused Should not change global semantics (except error message in pr_arg).
2020-02-22Preparing to simplifying the structure of type "tolerability".Hugo Herbelin
The "Any" case was not reached formerly for ETPattern and ETConstr as far as I can see. So there should be no change of semantics.
2020-02-21Merge PR #11590: Fixes #9741: only printing notations do not uselessly ↵Emilio Jesus Gallego Arias
reserve parsing keywords Reviewed-by: ejgallego
2020-02-21Merge PR #11642: Unconditionally print explanation for universe inconsistenciesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego
2020-02-21Merge PR #11142: Slightly improving strategy about when to print coercion or ↵Emilio Jesus Gallego Arias
explicitly print implicit arguments Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-02-21Adding changelog for #11590, fixing #9741.Hugo Herbelin
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
In particular, this fixes #9741.
2020-02-21Tactic_matching.pattern_match_term: remove ignored "refresh" argumentGaëtan Gilbert
It's been ignored since the introduction of universe polymorphism.
2020-02-21Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: herbelin
2020-02-21[merge-script] Improve warning in case of batch merging.Théo Zimmermann
2020-02-21Merge PR #11648: [test-suite] Fix output tests due to merge problems.Hugo Herbelin
Reviewed-by: herbelin
2020-02-20[test-suite] Fix output tests due to merge problems.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:11:01 +0000