aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-09Moving Gitlab CI documentation build to the main Coq build.Maxime Dénès
2018-03-09Integration of a sphinx-based documentation generator.Maxime Dénès
The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content.
2018-03-09Configure now fails with -with-doc yes when a doc dependency is missing.Maxime Dénès
2018-03-09Merge PR #6895: [compat] Remove "Refolding Reduction" option.Maxime Dénès
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-09Add an overlay for Equations and Ltac2.Pierre-Marie Pédrot
2018-03-09Fix compilation after the change of API in options.Pierre-Marie Pédrot
2018-03-09Documenting the Export modifier for options in CHANGES.Pierre-Marie Pédrot
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313.
2018-03-09Export the various option localities in the API.Pierre-Marie Pédrot
This prevents relying on an underspecified bool option argument.
2018-03-09doc and changes for coercion from prop/typecharguer
2018-03-09added test for coercion from typecharguer
2018-03-09allow Prop as source for coercionscharguer
2018-03-09Merge PR #6941: [toplevel] Respect COQ_COLORS environment variableMaxime Dénès
2018-03-09Merge PR #6945: Fix error with univ binders on monomorphic records.Maxime Dénès
2018-03-09Merge PR #6871: [build] Simpler byte/opt toplevel build.Maxime Dénès
2018-03-09Merge PR #6155: Get rid of ' notation for Zpos in QArithMaxime Dénès
2018-03-09Merge PR #6800: [checker] Printer cleanup.Maxime Dénès
2018-03-09Merge PR #6747: Relax conversion of constructors according to the pCuIC modelMaxime Dénès
2018-03-09Merge PR #6328: Fix #6313: lost goals in nested ltac in refineMaxime Dénès
2018-03-09Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesMaxime Dénès
2018-03-09Merge PR #6496: Generate typed generic code from ltac macrosMaxime Dénès
2018-03-09Merge PR #6937: Add empty compat file for Coq 8.8Maxime Dénès
2018-03-09Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵Maxime Dénès
fiat-crypto/OSX
2018-03-08More examples about shelve/given_up in tactic-in-terms.Hugo Herbelin
2018-03-08Cosmetic: add an expected newline in proof_global.Hugo Herbelin
2018-03-08A comment in Proofview.with_shelf.Hugo Herbelin
2018-03-08Add an invariant on future goals in Proof.run_tactic.Hugo Herbelin
More precisely, we check that future goals retrieved in run_tactic have no given_up goals since given_up goals are supposed to be produced only by Proofview.given_up and put on the given_up store. Doing the same for the shelf does not work: there is a situation where run_tactic ends where the same goal is both in the comb and on the shelf. This is when calling "clear x" on a goal "x:A |- ?p:B(?q[x])" when the dependent goal "x:A |- ?q:C" is not on the shelf. Tactic "clear" creates "|- ?p':B(?q'[])" and "|- ?q':C". The "advance" thing sees that the new comb is now composed of ?p' and ?q' but ?q' is a future goal which is later collected on the shelf (which ?q' is also in the comb). I tried to remove this redundancy but apparently it is necessary. There is an example in HoTT (file Classes/theory/rational.v) which requires this redundancy. I did not investigate why: the dependent evar is created by ring as part of a big term. So, as a conclusion, I kept the redundancy.
2018-03-08Add an invariant on given up goals in class_tactics.Hugo Herbelin
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
Tactic-in-term can be called from within a tactic itself. We have to preserve the preexisting future_goals (if called from pretyping) and we have to inform of the existence of pending goals, using future_goals which is the only way to tell it in the absence of being part of an encapsulating proofview. This fixes #6313. Conversely, future goals, created by pretyping, can call ltac:(giveup) or ltac:(shelve), and this has to be remembered. So, we do it.
2018-03-08Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.Hugo Herbelin
Adding also tclSETSHELF/tclGETSHELF by consistency with tclSETGOALS/tclGETGOALS. However, I feel that this is too low-level to be exported as a "tcl". Doesn't a "tcl" mean that it is supposed to be used by common tactics? But is it reasonable that a common tactic can change and modify comb and shelf without passing by a level which e.g. checks that no goal is lost in the process. So, I would rather be in favor of removing tclSETGOALS/tclGETGOALS which are anyway aliases for Comb.get/Comb.set. Conversely, what is the right expected level of abstraction for proofview.ml?
2018-03-08Add function bind in option.ml.Hugo Herbelin
2018-03-08Proof engine: using save_future_goal when relevant.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 23:36:07 +0000