aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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-04Merge PR #10265: Fix #10264: Singleton class field data is erroneous.Matthieu Sozeau
Reviewed-by: mattam82
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-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
2019-06-04instance_name grammar entry isn't globalGaëtan Gilbert
Not needed since we don't allow anonymous Declare Instance anymore (was needed for factorization or some such before that I think)
2019-06-04rewrite.ml: drop the id returned by new_instance earlierGaëtan Gilbert
We never use this id in rewrite.ml so don't bother threading it around.
2019-06-03Apparently unused ssr nonterminalsJim Fehrle
2019-06-03Merge branch 'master' of https://github.com/coq/coqJim Fehrle
2019-06-03Merge PR #10287: Update tutorial plugin to use sigma instad of evd, in ↵Enrico Tassi
keeping with doc recommendations Reviewed-by: gares
2019-06-03Merge PR #10280: Fixed typo in CONTRIBUTING.mdThéo Zimmermann
Reviewed-by: Zimmi48
2019-06-03Merge PR #10277: Remove Show Script (deprecated in 8.10)Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
2019-06-03Merge PR #10261: Update doc to reflect that PG now supports Coq-generated ↵Théo Zimmermann
proof diffs Reviewed-by: Zimmi48 Reviewed-by: cpitclaudel Ack-by: erikmd
2019-06-03Fix affiliation and ordering in CREDITSTalia Ringer
2019-06-03Update tutorial plugin to use sigma, in keeping with doc recommendationsTalia Ringer
2019-06-03Merge PR #10269: Checker: don't use monomorphic universes attached to a constantPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-06-03Update doc to reflect that PG now supports Coq-generated proof diffsJim Fehrle
2019-05-31Fixed typo in CONTRIBUTING.mdJose Fernando Lopez Fernandez
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-31Fix #10268: vio2vo produces incorrect term when discharging.Pierre-Marie Pédrot
We do not partially abstract the section info. Instead, we reuse the same code in cook_constr and cook_constant and pass the same section info.
2019-05-30Merge PR #10269: Checker: don't use monomorphic universes attached to a constantPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-05-29Merge PR #10252: Various dynamic assertions and cleanups in opaque typingMaxime Dénès
Reviewed-by: SkySkimmer Reviewed-by: maximedenes Ack-by: ppedrot
2019-05-29Merge PR #10248: Move the Discharge module in the kernel and merge it with ↵Maxime Dénès
Cooking Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: maximedenes Ack-by: ppedrot
2019-05-29Merge PR #10270: Fix debug printersEnrico Tassi
Reviewed-by: gares
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:32:04 +0000