vernac · coq · Tangled

forked from coq/coq

coq vernac

120 files

coqbot-app[bot] · Merge PR #22647: Print Universes Subgraph: keep the constraints with Set · 2w ago

Fix module lookup piercing opaque module type in Print Assumptions

assumptions.mli

Use the now correct set and maps Names APIs.

Move univ poly option to synterp

feat: Add elaboration of fresh qualities

auto_ind_decl.ml

Do not store recursive trees anymore in inductive blocks.

auto_ind_decl.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

lib.ml reduce dependence on Global

Update the OCaml headers to reflect the fact Coq is now Rocq.

Abstract away the Summary reference type.

Pass mode to class observer

comArguments.ml

[notation] Implement deep %scope in Arguments

comArguments.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

comAssumption.ml

Correctly pass side-effects in some Declare internals.

comAssumption.mli

Introduce PolyFlags to gather flags for polymorphic defs

Remove the name field from projections.

comCoercion.mli

Remove the deprecated nonuniform attribute

comDefinition.ml

Rename evar_universe_context into ustate

comDefinition.mli

Introduce PolyFlags to gather flags for polymorphic defs

comExtraDeps.ml

Abstract away the Summary reference type.

comExtraDeps.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Install hooks when attributes are completed

comFixpoint.mli

Install hooks when attributes are completed

Make the Dumpglob API more algebraic.

Introduce PolyFlags to gather flags for polymorphic defs

comInductive.ml

Extrude universe abstraction of inductive types out of the kernel.

comInductive.mli

Introduce "Univ@{s;l}" notation for sort polymorphism

comPrimitive.ml

Rename evar_universe_context into ustate

comPrimitive.mli

Revert name change of univ_decl to sort_poly_decl

comRewriteRule.ml

QGlobal is not QVar

comRewriteRule.mli

feat: Add elaboration of fresh qualities

Use the now correct set and maps Names APIs.

Use full_path for absolute paths more consistently

Undeprecate `...` ("Proof with")

Deprecate "end tac" ("...")

Update the OCaml headers to reflect the fact Coq is now Rocq.

Rename Coq -> Rocq in various comments and doc

Correctly pass side-effects in some Declare internals.

Turn Suggest Proof Using into a warning and add quickfix

Add Scheme All Command

Add Scheme All Command

Correctly handle "with Module" for functors in Declaremods.

declaremods.mli

Require: load kernel data outside the libobject system

Add warning when declaring redundant sort constraints

declareUniv.mli

Revert name change of univ_decl to sort_poly_decl

Remove compat coq-core libraries (not executables)

CLexer.terminal does not check keyword state

Procq APIs support ignoring keyword effects, use for SSR instead of unfreezing

Turn notation into a record

Qualified names for custom entries

Rename Coq -> Rocq in future message

Fix the stale marshalling comment on Future.computation

g_obligations.mlg

Do not return progress information in Declare obligation functions.

g_obligations.mli

Move g_obligations to vernac/ from ltac plugin

Add `Hint Mode =` to freeze corresponding evars in TC queries

Rename the Pcoq module into Procq.

Rename Coq -> Rocq in various comments and doc

Rename the Pcoq module into Procq.

Add `Print Height ident.` command. - Prints the definitional height of a given constant. - Also adds `Print Heights.`, which prints the heights of all the constants in scope.

Make `f (x:=e)%s` parse as `f (x:=e%s)` instead of `(f (x:=e))%s`

Fix recursive-call errors in fixpoint binder types

Update the OCaml headers to reflect the fact Coq is now Rocq.

Collapse sort variables to Prop if they are >= Prop but not <= Type

Add Scheme All Command

Library: fix library_is_loaded always returning true

Move print-mod-uid to main rocq exe instead of rocq repl

Abstract away the Summary reference type.

Move Flags.load_vos_libraries to Loadpath

Turn notation into a record

Infrastructure for printing non-flattened grammar structure

Abstract away the Summary reference type.

Mltop cache_obj API with interp phase

Use Option.get, join has already forced the future.

Document Opaques.Summary.join and inline

Merge PR #22528: Add constant unfolding heuristic based on definitional heights.

Qualified names for custom entries

Merge PR #22594: More informative printing of template universes

Fix instance argument to Print and About with sort_variables

printing: warn when module contents cannot be printed

Fix instance argument to Print and About with sort_variables

Move the goal-printing functions to vernac.

proof_diffs.mli

Move the goal-printing functions to vernac.

Nicer error for incorrect Proof using

proof_using.mli

Nicer error for incorrect Proof using

Gentactic hide that the underlying implem is genarg based

Gentactic hide that the underlying implem is genarg based

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Use the now correct set and maps Names APIs.

feat: Add elaboration of fresh qualities

Keep track of variable status (secvar or not) in named contexts

retrieveObl.mli

Rocqify the core.

Stop iterating through libobjects for Search

Fix Search Kind Bug

Make the Dumpglob API more algebraic.

Mltop cache_obj API with interp phase

tactic_option.ml

Abstract away the Summary reference type.

tactic_option.mli

tactic_option uses Gentactic

Update Topfmt.with_output_to_file to use memprof masking API

Delete unused Topfmt.deep_ft

vernac_classifier.ml

Add Scheme All Command

vernac_classifier.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

vernacControl.ml

update messages

vernacControl.mli

Properly handle `Timeout x Fail cmd`

vernacentries.ml

Print Universes Subgraph: keep the constraints with Set

vernacentries.mli

Export the locations of universes and the universe subgraph

Add `Print Height ident.` command. - Prints the definitional height of a given constant. - Also adds `Print Heights.`, which prints the heights of all the constants in scope.

vernacextend.ml

CLexer.terminal does not check keyword state

vernacextend.mli

Procq APIs support ignoring keyword effects, use for SSR instead of unfreezing

Move the goal-printing functions to vernac.

Move the goal-printing functions to vernac.

vernacinterp.ml

Fix state handling in Load

vernacinterp.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

vernacoptions.ml

Generalize MakeTable to handle mixed keys.

vernacoptions.mli

Redesign Goptions API

Add grammar entry for control flags instead of inlined list parsing

Update the OCaml headers to reflect the fact Coq is now Rocq.

[core] Improved state protection against memprof-limits interruptions

vernacstate.mli

Deprecate "end tac" ("...")

missing-proof-command warning mentions Default Proof Using if relevant

vernactypes.mli

Warning for missing "Proof" command and error on duplicate or late "Proof"