aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
2020-08-28Merge PR #12890: ring: generate fresh names for lemmascoqbot-app[bot]
2020-08-28Merge PR #11742: [numeral] [plugins] Remove Coq's `Bigint` module in favor of...coqbot-app[bot]
2020-08-28When reporting an implicit argument error on a rename argument, use the renam...Hugo Herbelin
2020-08-27[nsatz] num → zarithVincent Laporte
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-08-27Remove a call to the old refiner in ssr.Pierre-Marie Pédrot
2020-08-27tacinterp mini cleanup useless letinGaëtan Gilbert
2020-08-25omega: stop using intro_usingGaëtan Gilbert
2020-08-25funind: stop using intro_usingGaëtan Gilbert
2020-08-25ring: generate fresh names for lemmasGaëtan Gilbert
2020-08-23Merge PR #12851: Extraction: At declaration point of a global, use its declar...Maxime Dénès
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
2020-08-19Prefer eval_tactic_ist, which has error localisation, to interp_tactic.Hugo Herbelin
2020-08-19In tacinterp.ml, renaming eval_tactic into eval_tactic_ist to match the API.Hugo Herbelin
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
2020-08-18Extraction: At declaration point of a global, use its declaring name.Hugo Herbelin
2020-08-18Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152).Hugo Herbelin
2020-08-11Merge PR #12815: [micromega] Fix bug#12790Vincent Laporte
2020-08-11Merge PR #12814: [zify] fix for bug#12791Vincent Laporte
2020-08-10[micromega] Fix bug#12790Frédéric Besson
2020-08-10[zify] fix for bug#12791Frédéric Besson
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-07-18Merge PR #12696: [gramlib] Remove legacy located exception wrapper in favor o...Pierre-Marie Pédrot
2020-07-17Do not store the full environment inside ssr ast_closure_term.Pierre-Marie Pédrot
2020-07-16[gramlib] Remove legacy located exception wrapper in favor of standard infras...Emilio Jesus Gallego Arias
2020-07-08declare: Add [save_regular] API for obligation-ignoring proofsGaëtan Gilbert
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-29Remove the deprecated functions from refiner, moving them to Tacticals.Pierre-Marie Pédrot
2020-06-26[declare] Return list of declared global in Proof.saveEmilio Jesus Gallego Arias
2020-06-26[declare] Remove Proof_ending from the public APIEmilio Jesus Gallego Arias
2020-06-26[declare] Merge remaining obligations bits into DeclareEmilio Jesus Gallego Arias
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
2020-06-26[declare] Move udecl to Info structure.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:41:38 +0000