aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-24Merge PR #11560: Fix #11549: Ltac2 is incompatible with $.Tej Chajed
Reviewed-by: tchajed
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-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
This PR is in preparation of #9067 (together with #11647) . Before this PR, `grammar_extend` always took an optional `reinit` argument, even if it was never set to `Some ...`. Indeed, there is a single case where reinit is needed; we track it now by using a different extension rule constructor.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:18:18 +0000