aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Integration of a sphinx-based documentation generator.Gravatar Maxime Dénès2018-03-09
| | | | | | | | 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.
* Configure now fails with -with-doc yes when a doc dependency is missing.Gravatar Maxime Dénès2018-03-09
|
* Merge PR #6800: [checker] Printer cleanup.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6747: Relax conversion of constructors according to the pCuIC modelGravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6328: Fix #6313: lost goals in nested ltac in refineGravatar Maxime Dénès2018-03-09
|\ \ \
* \ \ \ Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Maxime Dénès2018-03-09
|\ \ \ \
* \ \ \ \ Merge PR #6496: Generate typed generic code from ltac macrosGravatar Maxime Dénès2018-03-09
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6937: Add empty compat file for Coq 8.8Gravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵Gravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | fiat-crypto/OSX
| | | | | * | | More examples about shelve/given_up in tactic-in-terms.Gravatar Hugo Herbelin2018-03-08
| | | | | | | |
| | | | | * | | Cosmetic: add an expected newline in proof_global.Gravatar Hugo Herbelin2018-03-08
| | | | | | | |
| | | | | * | | A comment in Proofview.with_shelf.Gravatar Hugo Herbelin2018-03-08
| | | | | | | |
| | | | | * | | Add an invariant on future goals in Proof.run_tactic.Gravatar Hugo Herbelin2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | * | | Add an invariant on given up goals in class_tactics.Gravatar Hugo Herbelin2018-03-08
| | | | | | | |
| | | | | * | | Proof engine: support for nesting tactic-in-term within other tactics.Gravatar Hugo Herbelin2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | * | | Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.Gravatar Hugo Herbelin2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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?
| | | | | * | | Add function bind in option.ml.Gravatar Hugo Herbelin2018-03-08
| | | | | | | |
| | | | | * | | Proof engine: using save_future_goal when relevant.Gravatar Hugo Herbelin2018-03-08
| | | | | | | |
| | | | | * | | Proof engine: adding a function to save future goals including principal one.Gravatar Hugo Herbelin2018-03-08
| | | | | | | |
| | | | | * | | Proof engine: consider the pair principal and future goals as an entity.Gravatar Hugo Herbelin2018-03-08
| |_|_|_|/ / / |/| | | | | |
* | | | | | | Merge PR #6522: Fix core hint database issue #6521Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6928: gitlab: install num for all 4.06 jobsGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | wish #4129)
* \ \ \ \ \ \ \ \ \ \ Merge PR #6893: Cleanup UState API usageGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
| |_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | | | Merge PR #6918: romega: get rid of EConstr.UnsafeGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6817: [configure]: support for profilesGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | | Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | | | | | | | | | | * | Add test-suite file for cumulative constructorsGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | |
| | | | | | | | | | | * | Leave cumul constructor universes as is during unifGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | if we cannot coerce one constructor type to the other. By invariant they have a common supertype
| | | | | | | | | | | * | Update checker to reflect rule on constructors of polymorphic inductive typesGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | |
| | | | | | | | | | | * | Relax conversion of constructors according to the pCuIC modelGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Nothing to check in conversion as they have a common supertype by typing. - In inference, enforce that one is lower than the other.
* | | | | | | | | | | | | Merge PR #6743: Add notation {x & P} for sigTGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6927: Add some missing flushes in configure.Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6881: [windows] support -addon in build scriptGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6933: Standard headers for C and Python.Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6934: Warn when using “Require” in a sectionGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6924: Clean-up remove always false useeager argument.Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6902: [compat] Remove "Discriminate Introduction"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6903: [compat] Remove "Shrink Abstract"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | * | | | | | | gitlab: install num for all jobsGravatar Gaëtan Gilbert2018-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously it was installed for the compilation jobs causing random failures when the other jobs got a cache without it.
| | | | | | | | | | | | | | | | | | | | | | | * [checker] Printer cleanup.Gravatar Emilio Jesus Gallego Arias2018-03-07
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Makes printing rules more explicit and should close #6799.
| | | | | * | | | | | | | | | | | | | | | | | Use a proper warning when a summary is captured out of module scope.Gravatar Vincent Laporte2018-03-07
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | | | | | | [vernac] Warn when using “Require” in a sectionGravatar Vincent Laporte2018-03-07
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | | | | | | [stdlib] Do not use “Require” inside sectionsGravatar Vincent Laporte2018-03-07
| |_|_|_|/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 05:23:34 +0000