aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-06-08Fix #10339: Anomaly in Ltac2.Pierre-Marie Pédrot
We use a user-facing wrapper instead of a low-level function raising internal exceptions.
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ↵Pierre-Marie Pédrot
interpretation scopes Reviewed-by: Zimmi48 Reviewed-by: ppedrot Ack-by: vbgl
2019-06-07Merge PR #10236: Update coqdev-setup-proofgeneral for duneEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: ejgallego
2019-06-07Merge PR #10330: Dune: run coqc with -w +defaultEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-07Merge PR #10335: simple IO CI branch is now `master`Emilio Jesus Gallego Arias
2019-06-07Merge PR #10311: Ltac2 codeowner / changelogMaxime Dénès
Reviewed-by: maximedenes
2019-06-07simple IO CI branch is now `master`Gaëtan Gilbert
2019-06-07Merge PR #10308: Merge the two sources of monomorphic constraints for ↵Gaëtan Gilbert
side-effects Reviewed-by: SkySkimmer
2019-06-07Dune: run coqc with -w +defaultGaëtan Gilbert
This matches the makefile build with -warn-error.
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Merge PR #10304: Clean up tuto0 and tuto1 to use better practices and ↵Pierre-Marie Pédrot
explain more Ack-by: SkySkimmer Reviewed-by: gares Reviewed-by: ppedrot Ack-by: tlringer
2019-06-06Merge PR #10278: vernac_load doesn't get a ?proof argumentEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: gares
2019-06-06Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.Vincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Reviewed-by: maximedenes Reviewed-by: vbgl
2019-06-06Merge PR #10323: Remove old overlaysEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-06Merge the two sources of monomorphic constraints for side-effects.Pierre-Marie Pédrot
Instead of having the monormorphic universes from the immediate data separated from the ones from the body, we only rely on the former. There is no reason to delay given that the body is always force upfront.
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-06Remove old overlaysGaëtan Gilbert
I updated the readme example using the most recent overlay with only 1 touched development.
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-05Add Andreas Lynge to CREDITSAndreas Lynge
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:43:04 +0000