aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-24added sphinx docAbhishek Anand (optiplex7010@home)
2020-02-24added changelogAbhishek Anand (optiplex7010@home)
2020-02-23Adding tests for Set Printing Parentheses.Hugo Herbelin
2020-02-23Cancelling precedences in Set Printing Parentheses only at border of notations.Hugo Herbelin
2020-02-23Adding a Display Parentheses menu in CoqIDE.Hugo Herbelin
2020-02-23Not iterating recursive notations more than once.Hugo Herbelin
2020-02-23parens --> parenthesesAbhishek Anand (optiplex7010@home)
2020-02-23bugfix: switched then/else: parens option false (default)=> no parensAbhishek Anand (optiplex7010@home)
2020-02-23added the new optionAbhishek Anand (optiplex7010@home)
2020-02-23patched the print functionAbhishek Anand (optiplex7010@home)
2020-02-23Merge pull request #11629 from ppedrot/fix-11552Tej Chajed
Fix #11552: Ltac2 breaks query commands during proofs.
2020-02-22Merge PR #11651: [merge-script] Improve warning in case of batch merging.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
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-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
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-20[init] Add `-boot` option to avoid binding `Coq.` prefix.Emilio Jesus Gallego Arias
This is useful when we want to have finer control of the location of files in the bootstrap process, for example when building using Dune. Also, this makes options consistent with what `coqdep` already uses for bootstrap. The main use case for `-boot` is to replace the hardcoded `add_load_path (coqlib () / theories)` with `-R dir Coq`, where dir is controlled by the build system. In particular, we use `-R . Coq` as we `cd` into the directory the package is, so without boot we'd have to hardcode the `theories` path in Dune itself. which seems less robust. Notably after this change the only part of the build that uses `coqlib` is the micromega solver, but that can be tweaked so if coqlib is not set it will use the one in the path. IMO not having to set "coqlib" is a good property if we want a more compositional setup.
2020-02-21Merge PR #11329: Fixing #11114: anomaly with Extraction Implicit on records.Kazuhiko Sakaguchi
Reviewed-by: pi8027
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-20Merge PR #11616: [coqdep] Tweak changelog after recent PRs.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2020-02-20Merge PR #11633: Add doc/unreleased.rst to .gitignore.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-20Merge PR #11630: [make] Fix makefile variable after plugin .v files moveGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2020-02-20Merge PR #11612: CoqIDE: allow opening multiple files at onceHugo Herbelin
2020-02-20Adding changelog.Hugo Herbelin
2020-02-20Fixing #11114 (anomaly with Extraction Implicit on records).Hugo Herbelin
This was due to an inconsistency in handling implicit arguments in the fields and in the constructor of a record.
2020-02-20Fixes #10917 (missing lift in building return clause by inversion).Hugo Herbelin
2020-02-20Adding a printer for GlobEnv in ocamldebug.Hugo Herbelin
2020-02-19Merge PR #11499: Clarify expectations for overlay creationEmilio Jesus Gallego Arias
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-02-19Merge PR #11302: Add --fuzz, --real, --user to timing scriptsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: jfehrle
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-19Overlays for Equations, QuickChick and Iris.Hugo Herbelin
2020-02-19Adding change log for #10832.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:06:14 +0000