aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-06-06Merge PR #10299: Lazy substitution of section contexts in opaque proofsMaxime Dénès
Reviewed-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-06-06Fix panel behavior as requested by #10292Claude Stolze
2019-06-06Remove old overlaysGaëtan Gilbert
I updated the readme example using the most recent overlay with only 1 touched development.
2019-06-06Update changes.rst as a follow-up to #9743Kazuhiko Sakaguchi
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ↵Gaëtan Gilbert
Type's argument Reviewed-by: SkySkimmer Reviewed-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-06-06Clean, document, and expand plugin tutorials 0 and 1Talia Ringer
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06Merge PR #10305: Fix SSR (un)fold of polymorphic terms - issue 9336Enrico Tassi
Reviewed-by: gares
2019-06-06Merge PR #10302: Fix SSR 'case B:b' with universe polymorphic equalityEnrico Tassi
Ack-by: andreaslyn Reviewed-by: gares
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter.
2019-06-05Add Andreas Lynge to CREDITSAndreas Lynge
2019-06-05Remove redundancies in the INSTALL doc.Théo Zimmermann
2019-06-05Changelog entry for Ltac2 (missing from #10002).Théo Zimmermann
2019-06-05Add codeowner for Ltac2. Forgotten in #10002.Théo Zimmermann
Who should be secondary owner?
2019-06-05Fix #10283: clearer dependency documentation for building CoqIDE.Théo Zimmermann
2019-06-05vernac_load doesn't get a ?proof argumentGaëtan Gilbert
AFAICT the stm never gives Load a non-None ?proof.
2019-06-05Merge PR #10215: Refine typing of vernacular commandsMaxime Dénès
Reviewed-by: SkySkimmer Ack-by: ejgallego Ack-by: gares
2019-06-05Merge PR #10307: allow empty tactic_rules in ARGUMENT EXTENDPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-06-05Merge PR #10296: Unused ssr ntsEnrico Tassi
Reviewed-by: gares
2019-06-05allow empty tactic_rules in ARGUMENT EXTENDDabrowski
2019-06-04[vernac] Interpret regular vernacs symbolicallyEmilio Jesus Gallego Arias
This provides uniformity to the inner loop and prepares the way to export a refined type for interpretation. The only non-uniformity remaining is the one due to the `?proof` parameter; it won't be easy to fix due to upper layers issues. Note that this step is not yet fully satisfying, as a true typed `vernac_expr` definition is still not possible because of syntactic non-uniformity, in particular all the surgery done for `CoFixpoint` and `Instance` should be eliminated in favor of more refined AST tags. An interesting TODO is to handle attributes symbolically too, as to remove boilerplate.
2019-06-04Fix SSR (un)fold of polymorphic terms - issue 9336Andreas Lynge
2019-06-04Merge PR #10265: Fix #10264: Singleton class field data is erroneous.Matthieu Sozeau
Reviewed-by: mattam82
2019-06-04Fix SSR 'case B:b' with universe polymorphic equalityAndreas Lynge
2019-06-04Fix typo in changelogEnrico Tassi
2019-06-04Simplify vernacentries calls to classes, remove unused args, reject ↵Gaëtan Gilbert
deprecated attribute This code was significantly more complex than necessary.
2019-06-04[rewrite] remove program_mode from attributes (unused)Enrico Tassi
2019-06-04remove leftover commentsEnrico Tassi
2019-06-04update overlaysEnrico Tassi
2019-06-04[classes] remove program mode from the new_instance_* APIsEnrico Tassi
2019-06-04[vernac] more precise types for Add Morph, Instance, and FunctionEnrico Tassi
2019-06-04[vernac] remove VtMaybeOpenProofEnrico Tassi
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-04VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)Gaëtan Gilbert
+ hide interp_functional_vernac in vernacentries
2019-06-04Overlays for coq/coq#10050 (proof_global API changes)Gaëtan Gilbert
2019-06-04Replace ModifyProofStack by CloseProofGaëtan Gilbert
The only use of ModifyProofStack was in paramcoq for closing a proof.
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Rename Proof_global.{t -> stack}Gaëtan Gilbert
2019-06-04Vernacextend only returns a proof_global.t option, not a vernacstateGaëtan Gilbert
2019-06-04Funind: use maybe_open_proof a bit lessGaëtan Gilbert
2019-06-04Alternate syntax for ![]: VERNAC EXTEND Foo STATE proofGaëtan Gilbert
eg ![proof] becomes STATE proof This commits still supports the old ![] so there is redundancy: ~~~ VERNAC EXTEND Foo STATE proof | ... VERNAC EXTEND Foo | ![proof] ... ~~~ with the ![] form being local to the rule and the STATE form applying to the whole EXTEND except for the rules with a ![].
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
![proof_stack] is equivalent to the old meaning of ![proof]: the body has type `pstate:Proof_global.t option -> Proof_global.t option` The other specifiers are for the following body types: ~~~ ![open_proof] `is_ontop:bool -> pstate` ![maybe_open_proof] `is_ontop:bool -> pstate option` ![proof] `pstate:pstate -> pstate` ![proof_opt_query] `pstate:pstate option -> unit` ![proof_query] `pstate:pstate -> unit` ~~~ The `is_ontop` is only used for the warning message when declaring a section variable inside a proof, we could also just stop warning. The specifiers look closely related to stm classifiers, but currently they're unconnected. Notably this means that a ![proof_query] doesn't have to be classified QUERY. ![proof_stack] is only used by g_rewrite/rewrite whose behaviour I don't fully understand, maybe we can drop it in the future. For compat we may want to consider keeping ![proof] with its old meaning and using some new name for the new meaning. OTOH fixing plugins to be stricter is easier if we change it as the errors tell us where it's used.
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
Typically instead of [start_proof : ontop:Proof_global.t option -> bla -> Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and the pstate is pushed on the stack by a caller around the vernacentries/mlg level. Naming can be a bit awkward, hopefully it can be improved (maybe in a followup PR). We can see some patterns appear waiting for nicer combinators, eg in mlg we often only want to work with the current proof, not the stack. Behaviour should be similar modulo bugs, let's see what CI says.
2019-06-04Remove the discharge segment from vo files.Pierre-Marie Pédrot
Since the introduction of delayed section substitution, the opaque table was already containing the same information.
2019-06-04Slightly tweak the representation of dischargeable opaque proofs.Pierre-Marie Pédrot
This will allow an easier removal of the discharge segment in a later commit.
2019-06-04Do not substitute opaque constants when discharging.Pierre-Marie Pédrot
Instead we do that on a by-need basis by reusing the section info already stored in the opaque proof.
2019-06-04Merge PR #10276: Fix #10268: vio2vo produces incorrect term when discharging.Enrico Tassi
Reviewed-by: gares Ack-by: ppedrot
2019-06-04rewrite.ml: remove outdated commentGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-15 17:09:44 +0000