| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-08-17 | In docs, fix command to reset Ltac profiling | Paul Steckler | |
| 2016-08-16 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-08-04 | Fix documentation typo (bug #4994). | Guillaume Melquiond | |
| 2016-07-17 | More examples of recursive notations, with emphasis in reference manual. | Hugo Herbelin | |
| Further work would include: - Identify binders up to alpha-conversion (see #4932 with a list of binders of length at least 2, or #4592 on printing notations such as ex2). A cool example that one could also consider supporting: - Notation "[[ a , .. , b | .. | a , .. , b ]]" := (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..). | |||
| 2016-07-01 | Add and document match, fix and cofix reduction flags. | Maxime Dénès | |
| 2016-06-29 | Updated CHANGES about subst. More on recursive equations in reference manual. | Hugo Herbelin | |
| 2016-06-29 | Fixes in documentation. | Matthieu Sozeau | |
| 2016-06-29 | Program: cleanup in cases, add options | Matthieu Sozeau | |
| Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases. | |||
| 2016-06-28 | Merge remote-tracking branch 'github/pr/207' into trunk | Maxime Dénès | |
| Was PR#207: Add -no-print-dependent-evars | |||
| 2016-06-28 | Documenting the "only printing" notation flag. | Pierre-Marie Pédrot | |
| 2016-06-27 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-06-27 | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre | |
| Cf CHANGES for details. | |||
| 2016-06-20 | Reference Manual / Extraction: the original example command no longer works ↵ | Matej Kosik | |
| with recent Coq | |||
| 2016-06-19 | Add [Unset Printing Dependent Evars Line] | Jason Gross | |
| This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819. | |||
| 2016-06-17 | par: like all: but in parallel | Enrico Tassi | |
| This commit documents par:, fixes its semantics so that is behaves like all:, supports (toplevel) abstract and optimizes toplevel solve. `par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1` but is optimized for failures: if one goal fails all are aborted immediately. `par: abstract tac` runs abstract on the generated proof terms. Nested abstract calls are not supported. | |||
| 2016-06-16 | Document new Hint Mode option. | Matthieu Sozeau | |
| 2016-06-16 | Revise syntax of Hint Cut | Matthieu Sozeau | |
| As noticed by C. Cohen it was confusingly different from standard notation. | |||
| 2016-06-16 | Merge 'pr/191' into trunk | Enrico Tassi | |
| 2016-06-15 | typography | Matej Kosik | |
| 2016-06-14 | Add documentation for goal selectors. | Cyprien Mangin | |
| 2016-06-14 | -async-proofs-delegation-threshold default value set to 0.03 | Enrico Tassi | |
| Documentation also updated. | |||
| 2016-06-14 | Merge remote-tracking branch 'origin/pr/173' into trunk | Enrico Tassi | |
| This is the "error resiliency" mode for STM | |||
| 2016-06-14 | Merge branch "LtacProf for trunk" (PR #165). | Pierre-Marie Pédrot | |
| 2016-06-13 | Univs: more robust Universe/Constraint decls #4816 | Matthieu Sozeau | |
| This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816 | |||
| 2016-06-07 | typo | Matej Kosik | |
| 2016-06-07 | typography | Matej Kosik | |
| 2016-06-07 | Documentation | Enrico Tassi | |
| 2016-06-05 | Make Ltac Profiling an setting | Jason Gross | |
| 2016-06-05 | Synchronize the profiler state with the document | Jason Gross | |
| This is suboptimal, because mutation leaves room for subtle bugs, but rewriting @tebbi's code to be functional was a pain, and not something I could figure out how to do easily. I'm working under the assumption that there is no sharing in a single treenode, which I'm not completely sure is valid. That said, a few simple tests seem to indicate that this works as expected. | |||
| 2016-06-05 | -profileltac -> -profile-ltac, as per @herbelin | Jason Gross | |
| https://github.com/coq/coq/pull/150#issuecomment-219141596 ```bash git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i ``` | |||
| 2016-06-05 | Add LtacProf documentation | Jason Gross | |
| 2016-06-05 | Adding the Print Ltac Signature command. | Pierre-Marie Pédrot | |
| 2016-05-15 | Fix a really small doc typo | Ricky Elrod | |
| 2016-05-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-05-03 | In Regular Subst Tactic mode, ensure that the order of hypotheses is | Hugo Herbelin | |
| preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual. | |||
| 2016-04-24 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-04-12 | FIX: HTML version of Chapter 4 of the Reference Manual | Matej Kosik | |
| 2016-04-12 | TYPOGRAPHY: adding missing \noindent macros | Matej Kosik | |
| 2016-04-04 | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵ | Matthieu Sozeau | |
| into JasonGross-trunk-function_scope | |||
| 2016-03-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-02-24 | Document Hint Mode, cleanup Hint doc. | Matthieu Sozeau | |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-20 | Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500. | Maxime Dénès | |
| 2016-01-20 | Documenting Set Bullet Behavior. | Hugo Herbelin | |
| This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it. | |||
| 2016-01-20 | Clarifying the documentation of tactics "cbv" and "lazy". | Hugo Herbelin | |
| Following a discussion on coq-club on Jan 13, 2016. | |||
| 2016-01-15 | Thanks Hugo, but let's remain factual. | Maxime Dénès | |
| 2016-01-14 | Updating and improving the documentation of intros patterns. | Hugo Herbelin | |
| In particular, documenting bracketing of last pattern on by default. | |||
| 2016-01-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-12 | Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics. | Hugo Herbelin | |
| 2016-01-12 | Documenting dtauto and dintuition. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |