| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-07-10 | CHANGES: grammatical correction, suggested by Jason Gross on Bugzilla. | Maxime Dénès | |
| 2015-07-05 | More precise rewording about asymmetric patterns. | Hugo Herbelin | |
| 2015-06-26 | Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" | Lionel Rieg | |
| 2015-05-18 | Fixed CHANGES to reflect -color option. | Pierre Courtieu | |
| 2015-05-14 | Adding an option -w to control Coq warning output. | Pierre-Marie Pédrot | |
| For now, warnings are still ignored by default, but this may change. This commit at least allows to print them whenever desired. The -w syntax is also opened to future additions to further control the display of warnings. | |||
| 2015-05-13 | Safer typing primitives. | Pierre-Marie Pédrot | |
| Some functions from pretyping/typing.ml and their derivatives were potential source of evarmap leaks, as they dropped their resulting evarmap. This commit clarifies the situation by renaming them according to a unsafe_* scheme. Their sound variant is likewise renamed to their old name. The following renamings were made. - Typing.type_of -> unsafe_type_of - Typing.e_type_of -> type_of - A new e_type_of function that matches the e_ prefix policy - Tacmach.pf_type_of -> pf_unsafe_type_of - A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated. | |||
| 2015-05-13 | Documenting the Loose Hint Behavior flag. | Pierre-Marie Pédrot | |
| 2015-05-09 | Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for | Hugo Herbelin | |
| preserving compatibility of subst after #4214 being solved. | |||
| 2015-05-04 | Fix documentation of Redirect | Enrico Tassi | |
| 2015-04-22 | More precise numbers about Benjamin's fix for the VM. | Maxime Dénès | |
| 2015-04-22 | Update CHANGES | Matthieu Sozeau | |
| 2015-04-07 | Removing references to -I -as from CHANGES. | Pierre-Marie Pédrot | |
| 2015-04-01 | Accomodating #4166 (providing "Require Import OmegaTactic" as a | Hugo Herbelin | |
| replacement for 8.4's "Require Omega"). | |||
| 2015-03-22 | Announcing * and ** which were not official yet in 8.4. | Hugo Herbelin | |
| 2015-03-22 | Aliasing give_up with admit | Enrico Tassi | |
| 2015-03-13 | CHANGES: more correct equivalent to "constructor tac" syntax. | Arnaud Spiwack | |
| As mentionne in #3969, using "once (constructor;tac)" leads in exponential blowups, whereas "[> once (constructor;tac) ..]" does not. | |||
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | |
| - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit | |||
| 2015-02-28 | Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ↵ | Pierre Boutillier | |
| r15439 as we were talking at that time) | |||
| 2015-02-24 | CHANGES: Info command + info_auto currently broken. | Arnaud Spiwack | |
| 2015-02-15 | Undo: back to 8.4 semantics (Close #3514) | Enrico Tassi | |
| Only tactics are taken into account. | |||
| 2015-02-15 | Note about "Undo. Undo." in CHANGES | Enrico Tassi | |
| 2015-02-15 | Document the behavior change of Instance wrt {|...|}. (Fix for bug #3749) | Guillaume Melquiond | |
| 2015-02-13 | Document the issue with trivial inductive types. (Workaround for bug #3984) | Guillaume Melquiond | |
| 2015-02-12 | Fix typos about .vio files (thanks Arthur for spotting them) | Enrico Tassi | |
| 2015-01-24 | Updating CHANGES (grammar, thanks to AS for pointing it out) + | Hugo Herbelin | |
| a line on "Intuition Negation Unfolding". | |||
| 2015-01-23 | Typos, grammar, layout in CHANGES (continued). | Hugo Herbelin | |
| 2015-01-23 | Typos, grammar, layout in CHANGES. | Hugo Herbelin | |
| 2015-01-16 | Documenting the removal of coercions between sig, sigT, sig2, | Hugo Herbelin | |
| etc. (source of incompatibility). | |||
| 2015-01-15 | Move explanations about primitive projections to the manual. | Matthieu Sozeau | |
| 2015-01-15 | Update header of CHANGES. | Maxime Dénès | |
| 2015-01-15 | Mention guard condition in CHANGES. | Maxime Dénès | |
| 2015-01-14 | CHANGES: my recent updates to Ltac. | Arnaud Spiwack | |
| - gfail - multimatch - tryif/then/else | |||
| 2015-01-13 | More in CHANGES about local definitions | Pierre-Marie Pédrot | |
| 2015-01-10 | CHANGES: mention "Optimize (Heap|Proof)" | Enrico Tassi | |
| 2015-01-08 | Update + English in CHANGES | Hugo Herbelin | |
| 2015-01-08 | Start credits for 8.5. | Matthieu Sozeau | |
| 2015-01-08 | Fixed and extend bullet related info/error messages. + doc. | Pierre Courtieu | |
| Had to put some hook in the handler of Proofview.NoSuchgoals. Documentation updated. CHANGE updated. | |||
| 2015-01-08 | Document native_compute. | Maxime Dénès | |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi | |
| 2014-12-30 | Document the new behavior of lazymatch. | Guillaume Melquiond | |
| 2014-12-30 | more CHANGES | Enrico Tassi | |
| 2014-12-23 | Minor modification of CHANGE. | Pierre Courtieu | |
| 2014-12-19 | Better doc and a few fixes for Proof using. | Enrico Tassi | |
| 2014-12-16 | In CHANGES, alerting about stronger check on notation level modifiers. | Hugo Herbelin | |
| 2014-12-15 | About now accepts hypothesis names and goal selector. | Pierre Courtieu | |
| 2014-12-12 | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu | |
| Documentation also updated. | |||
| 2014-11-30 | Documenting the Set Refine Instance Mode. | Pierre-Marie Pédrot | |
| 2014-11-18 | Hopefully the last word on having "simpl f" complying with the | Hugo Herbelin | |
| semantics described in the reference manual (i.e. if "f" is a qualid, do not add implicit arguments and, a fortiori, do not try to solve these implicit arguments - in particular, changing DbLib which expected this rule not to be followed). | |||
| 2014-11-18 | Fixing detection of occurrences in the presence of nested subterms for | Hugo Herbelin | |
| "simpl at" and "change at". | |||
| 2014-11-17 | Documenting use of colors in Coq. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |