aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-08Proof engine: adding a function to save future goals including principal one.Hugo Herbelin
2018-03-08Proof engine: consider the pair principal and future goals as an entity.Hugo Herbelin
2018-03-08Merge PR #6522: Fix core hint database issue #6521Maxime Dénès
2018-03-08Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsMaxime Dénès
2018-03-08Merge PR #6928: gitlab: install num for all 4.06 jobsMaxime Dénès
2018-03-08Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵Maxime Dénès
wish #4129)
2018-03-08Merge PR #6893: Cleanup UState API usageMaxime Dénès
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895.
2018-03-08Make most of TACTIC EXTEND macros runtime calls.Maxime Dénès
Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros.
2018-03-08Merge PR #6918: romega: get rid of EConstr.UnsafeMaxime Dénès
2018-03-08coqide: queries from the query window are routed there (fix #5684)Enrico Tassi
We systematically use Wg_MessageView for both the message panel and each Query tab; we register all MessageView in a RoutedMessageViews where the default route (0) is the message panel. Queries from the Query panel pick a non zero route to have their feedback message delivered to their MessageView
2018-03-08Fix error with univ binders on monomorphic records.Gaëtan Gilbert
Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were declared twice for all records. Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an observable error for monomorphic records.
2018-03-08Merge PR #6817: [configure]: support for profilesMaxime Dénès
2018-03-08Fix SR breakage due to allowing fixpoints on non-rec valuesMatthieu Sozeau
We limit fixpoints to Finite inductive types, so that BiFinite inductives (non-recursive records) are excluded from fixpoint construction. This is a regression in the sense that e.g. fixpoints on unit records were allowed before. Primitive records with eta-conversion are included in the BiFinite types. Fix deprecation Fix error message, the inductive type needs to be recursive for fix to work
2018-03-08Add test-suite file for cumulative constructorsMatthieu Sozeau
2018-03-08Leave cumul constructor universes as is during unifMatthieu Sozeau
if we cannot coerce one constructor type to the other. By invariant they have a common supertype
2018-03-08Update checker to reflect rule on constructors of polymorphic inductive typesMatthieu Sozeau
2018-03-08Relax conversion of constructors according to the pCuIC modelMatthieu Sozeau
- Nothing to check in conversion as they have a common supertype by typing. - In inference, enforce that one is lower than the other.
2018-03-08Merge PR #6743: Add notation {x & P} for sigTMaxime Dénès
2018-03-08Merge PR #6927: Add some missing flushes in configure.Maxime Dénès
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-08Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Maxime Dénès
2018-03-08Merge PR #6881: [windows] support -addon in build scriptMaxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-08Merge PR #6933: Standard headers for C and Python.Maxime Dénès
2018-03-08Merge PR #6934: Warn when using “Require” in a sectionMaxime Dénès
2018-03-08Merge PR #6924: Clean-up remove always false useeager argument.Maxime Dénès
2018-03-08Merge PR #6902: [compat] Remove "Discriminate Introduction"Maxime Dénès
2018-03-08Merge PR #6903: [compat] Remove "Shrink Abstract"Maxime Dénès
2018-03-08Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Maxime Dénès
2018-03-07[toplevel] Respect COQ_COLORS environment variableThomas Hebb
Since 3fc02bb2034a ("[pp] Move terminal-specific tagging to the toplevel."), the COQ_COLORS environment variable has been ignored, since init_terminal_output unconditionally called init_tag_map with the default colors, overwriting any custom colors that had been previously set. Fix this by creating a separate function, default_styles, to set the default colors. Also, remove the clear_styles function, as it was only called in one place and did nothing (since tag_map is empty to begin with).
2018-03-07gitlab: install num for all jobsGaëtan Gilbert
Previously it was installed for the compilation jobs causing random failures when the other jobs got a cache without it.
2018-03-07[checker] Printer cleanup.Emilio Jesus Gallego Arias
Makes printing rules more explicit and should close #6799.
2018-03-07Use a proper warning when a summary is captured out of module scope.Vincent Laporte
2018-03-07[vernac] Warn when using “Require” in a sectionVincent Laporte
2018-03-07[stdlib] Do not use “Require” inside sectionsVincent Laporte
2018-03-07Add empty compat file for Coq 8.8Jason Gross
This closes #6598
2018-03-07Merge PR #6744: Add String.concatMaxime Dénès
2018-03-07Merge PR #6932: [stdlib] Do not use deprecated notationsMaxime Dénès
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-07Merge PR #6922: Remove outdated information regarding the FAQ.Maxime Dénès
2018-03-07Merge PR #6374: [toplevel] Modify printing goal strategy.Maxime Dénès
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-07Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Maxime Dénès
2018-03-06Add CHANGES and man entry for coqdep learning _CoqProject.Gaëtan Gilbert
2018-03-06Closes #6830: coqdep reads options and files from _CoqProject.Gaëtan Gilbert
Note that we don't look inside -arg for eg -coqlib.
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
2018-03-06Extraction: switch to EConstr.t as the central type to extract from.Pierre Letouzey
This is a bit artificial since the extraction normally operates on finished constrs (with no evars). But: - Since we use Retyping quite a lot, switching to EConstr.t allows to get rid of many `EConstr.Unsafe.to_constr (... (EConstr.of_constr ...))` - This prepares the way for a possible extraction of the content of ongoing proofs (a forthcoming `Show Extraction` command, see #4129 )
2018-03-06romega: get rid of EConstr.UnsafePierre Letouzey
We replace constr by EConstr.t everywhere, and propagate some extra sigma args
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-01 00:58:13 +0000