tactics · coq · Tangled

forked from coq/coq

coq tactics

72 files

Gaëtan Gilbert · Basic Info printing for apply and derived tactics (constructor etc) · 1mo ago

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

Add a deprecated option to restore the previous abstract behaviour.

Use the now correct set and maps Names APIs.

Remove duplicate warnings for missing all scheme

Remove the name field from projections.

Stop accepting non-globref hints from Hints.

Abstract away the Summary reference type.

autorewrite.mli

Improve backwards compatibility by making `forward` optional

Distinguish unapplied functions from other terms in the dnet

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

cbn delayed subst

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

class_tactics.ml

Better representation for no-mode case in Hints module

class_tactics.mli

parametrize typeclass functions with the db

contradiction.ml

Remove some spurious calls to pf_apply.

contradiction.mli

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

declareScheme.ml

Use the now correct set and maps Names APIs.

declareScheme.mli

Use the now correct set and maps Names APIs.

Remove unused API from Dn.

Remove unused API from Dn.

Remove compat coq-core libraries (not executables)

Use the now correct set and maps Names APIs.

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

Use variable status to decide if a variable is section variable

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

Reduce the exposure of QualityOrSet.t type in the Retyping API.

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

Use the now correct set and maps Names APIs.

elimschemes.mli

Add SProp case analysis scheme kinds (scase_dep, scase_nodep)

Reduce the exposure of QualityOrSet.t type in the Retyping API.

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

Compute cross-scheme universe constraints explicitly

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

Use the now correct set and maps Names APIs.

remove use of `option orientation` when only orientation is needed

evar_tactics.ml

Take a qualid in Evarnames.resolve.

evar_tactics.mli

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

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

refactor fixpoint tactics

Use variable status to decide if a variable is section variable

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

Make the Genredexpr.red_expr_gen type open-ended.

Added APIs for coqlsp

Added APIs for coqlsp

Use the now correct set and maps Names APIs.

Use the now correct set and maps Names APIs.

Remove dead API from Hipattern.

Remove dead API from Hipattern.

Use the now correct set and maps Names APIs.

generalize DeclareScheme from Constant.t to GlobRef.t

Fix generation of eliminators for not recursive inductive type but with non-unfiorm parameters

move indrec from pretpying/ to tactics/

Rename is_section_variable' -> is_section_variable_env

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

Reduce the exposure of QualityOrSet.t type in the Retyping API.

Remove the not extremely well-named Inv.inv function.

Make the Genredexpr.red_expr_gen type open-ended.

Make the Genredexpr.red_expr_gen type open-ended.

Abstract away the Summary reference type.

Make the Genredexpr.red_expr_gen type open-ended.

Make the Genredexpr.red_expr_gen type open-ended.

Make the Genredexpr.red_expr_gen type open-ended.

Abstract the result type of rewrite strategies and modulify it.

Abstract the result type of rewrite strategies and modulify it.

Remove APIs that have been deprecated before 9.0.

Stdarg.wit_identref is vernac_genarg_type

Reduce the exposure of QualityOrSet.t type in the Retyping API.

Remove APIs that have been deprecated before 9.0.

tacticErrors.ml

Report which terms are not convertible (#20944)

tacticErrors.mli

Report which terms are not convertible (#20944)

Basic Info printing for apply and derived tactics (constructor etc)

Report which terms are not convertible (#20944)