aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-11-15Merge PR #12611: [record] Cleanup of data structure and functionscoqbot-app[bot]
2020-11-15Moving the analysis of notation strings in notation.ml.Hugo Herbelin
2020-11-15Implement export locality for the remaining Hint commands.Pierre-Marie Pédrot
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
2020-11-13[record] Some documentation + minor refactoringEmilio Jesus Gallego Arias
2020-11-13[record] [ci] Overlay for elpiEmilio Jesus Gallego Arias
2020-11-13[record] Options API cleanup.Emilio Jesus Gallego Arias
2020-11-13[record] Refactor nested functions.Emilio Jesus Gallego Arias
2020-11-13[record] Cleanup of data structure and functions [2/2]Emilio Jesus Gallego Arias
2020-11-13[record] Cleanup of data structure and functions [1/2]Emilio Jesus Gallego Arias
2020-11-12Revert to "using" not being a keyword in -noinit mode.Théo Zimmermann
2020-11-12Add support for Proof using in -noinit mode.Théo Zimmermann
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...coqbot-app[bot]
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-10Merge PR #13322: [obligation] Properly handle no obligations on `Next Obligat...coqbot-app[bot]
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
2020-11-06Merge PR #13139: Clean the constr-as-hint APIcoqbot-app[bot]
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-05Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ...coqbot-app[bot]
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
2020-11-04Typing patterns and using type constraints in Search.Hugo Herbelin
2020-11-04Fixes #13298: primitive projections needs a correct typing environment.Hugo Herbelin
2020-11-04Moving interpretation of user-level universes in constrintern.ml.Hugo Herbelin
2020-11-04Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.Hugo Herbelin
2020-11-04Further code simplification in arbitrary hint interpretation.Pierre-Marie Pédrot
2020-11-04Do not try to be clever for term-as-hint interpretation.Pierre-Marie Pédrot
2020-11-04Opacify the Hints.hint_term type.Pierre-Marie Pédrot
2020-11-04Encapsulate the last use of IsConstr in the Hints API.Pierre-Marie Pédrot
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding not...coqbot-app[bot]
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-11-02document Proof.compactEnrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
2020-10-26Improve tactic interpreter registration API a bitGaëtan Gilbert
2020-10-23[declare] Remove recursive declaration from non-recursive functionsEmilio Jesus Gallego Arias
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
2020-10-19Addressing parsing part #13078.Hugo Herbelin
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-16Generalizing and exporting interp_assumption/interp_definition.Hugo Herbelin
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:40:10 +0000