| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-02-02 | ide: lablgtk fixes | slrnsc | |
| 2021-02-01 | Add changelog entry | slrnsc | |
| 2021-02-01 | ide: shift+enter to find backwards | slrnsc | |
| 2021-01-28 | Merge PR #13799: Replace : term with : type in open binders. | coqbot-app[bot] | |
| Reviewed-by: jfehrle | |||
| 2021-01-28 | Merge PR #13789: Document limitation of rewrite regarding occurrence selection. | coqbot-app[bot] | |
| Reviewed-by: jfehrle Reviewed-by: silene | |||
| 2021-01-28 | Update doc/sphinx/proofs/writing-proofs/rewriting.rst | Jim Fehrle | |
| 2021-01-28 | Merge PR #13781: [micromega] Deprecate hopefully useless options and flags | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 Ack-by: jfehrle | |||
| 2021-01-28 | Replace : term with : type in open binders. | Théo Zimmermann | |
| And update the doc_grammar files. | |||
| 2021-01-28 | Apply suggestions from code review | Théo Zimmermann | |
| Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 2021-01-28 | Merge PR #13763: Remove the SearchHead command (deprecated in 8.12) | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2021-01-28 | Merge PR #13790: [vernac] Check that no proofs do remain open at ↵ | coqbot-app[bot] | |
| section/module closing time Reviewed-by: SkySkimmer | |||
| 2021-01-28 | Document how rewrite works regarding occurrence selection. | Théo Zimmermann | |
| 2021-01-27 | Merge PR #13418: [sysinit] new component | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: JasonGross | |||
| 2021-01-27 | Typo in comment | Gaëtan Gilbert | |
| Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr> | |||
| 2021-01-27 | Add sysinit to load_printer lists | Gaëtan Gilbert | |
| 2021-01-27 | make the linter happy | Enrico Tassi | |
| 2021-01-27 | [coqargs] use standard option injection for -print-emacs | Enrico Tassi | |
| 2021-01-27 | [coqargs] use standard option injection for -type-in-type | Enrico Tassi | |
| 2021-01-27 | [coqargs] use standard option injection for -mangle-names | Enrico Tassi | |
| 2021-01-27 | [coqtop] handle -print-module-uid after initialization | Enrico Tassi | |
| 2021-01-27 | [coqc] move -output-context from sysinit/coqargs to coqc proper | Enrico Tassi | |
| 2021-01-27 | [sysinit] move initialization code from coqtop to here | Enrico Tassi | |
| We also spill (some) non-generic arguments and initialization code out of coqargs and to coqtop, namely colors for the terminal. There are more of these, left to later commits. | |||
| 2021-01-27 | [sysinit] new component for system initialization | Enrico Tassi | |
| This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml | |||
| 2021-01-27 | [vernac] move vernac_classifier to vernac | Enrico Tassi | |
| 2021-01-27 | [ltac] break dependency on the STM | Enrico Tassi | |
| 2021-01-27 | Merge PR #13785: [coqargs] use the standard option injection system for -w | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Ack-by: Zimmi48 | |||
| 2021-01-26 | Merge PR #13771: Slightly less stupid algorithm for simpl fixpoint expansion ↵ | coqbot-app[bot] | |
| + cleanups Reviewed-by: mattam82 | |||
| 2021-01-26 | [coqargs] use option injection for -w | Enrico Tassi | |
| 2021-01-26 | [options] improve support for append | Enrico Tassi | |
| 2021-01-26 | [vernac] Check that no proofs do remain open at section/module closing time | Emilio Jesus Gallego Arias | |
| Fixes #13755 . | |||
| 2021-01-26 | Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12) | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2021-01-26 | Merge PR #13773: Add missing item about PDF manual to release checklist. | coqbot-app[bot] | |
| Reviewed-by: ejgallego Reviewed-by: gares | |||
| 2021-01-25 | Remove the SearchHead command | Jim Fehrle | |
| 2021-01-25 | Remove the Hide Obligations flag | Jim Fehrle | |
| 2021-01-25 | Merge PR #13779: Properly implement local references in Summary. | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2021-01-25 | add test | Enrico Tassi | |
| 2021-01-25 | Update doc/changelog/04-tactics/13781-deprecate_micromega_options.rst | Frédéric Besson | |
| Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 2021-01-25 | Update doc/sphinx/addendum/micromega.rst | Frédéric Besson | |
| Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 2021-01-24 | Merge PR #13762: Remove double induction tactic | Pierre-Marie Pédrot | |
| Ack-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2021-01-22 | changelog | BESSON Frederic | |
| 2021-01-22 | Merge PR #13754: Improve doc of occurrences and rewrite. | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 | |||
| 2021-01-22 | [micromega] Deprecate hopefully useless options and flags | BESSON Frederic | |
| The goal is to eventually only use the Simplex solver and remove all the code needed for fourier elimination. | |||
| 2021-01-22 | Improve doc of occurrences and rewrite. | Jim Fehrle | |
| 2021-01-22 | Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11) | Pierre-Marie Pédrot | |
| Reviewed-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2021-01-22 | Properly implement local references in Summary. | Pierre-Marie Pédrot | |
| 2021-01-22 | Merge PR #13775: Improve wording for #13384 (Warn on hints without an ↵ | coqbot-app[bot] | |
| explicit locality) Reviewed-by: Zimmi48 | |||
| 2021-01-21 | Improve wording for #13384 | Jim Fehrle | |
| 2021-01-21 | Add missing item about PDF manual to release checklist. | Théo Zimmermann | |
| 2021-01-21 | Merge PR #13764: Remove Add InjTyp and 10 other micromega commands ↵ | BESSON Frederic | |
| (deprecated in 8.13) Reviewed-by: Zimmi48 Reviewed-by: fajb | |||
| 2021-01-21 | Merge PR #13770: Fix: `@tactic` is not a tactic, so can't begin a .. tacn:: | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |