| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-08-26 | Add a regression test for 3427 | Jason Gross | |
| 2014-08-26 | Prove forall extensionality | Jason Gross | |
| 2014-08-26 | Add t-jagro to .mailmap | Jason Gross | |
| 2014-08-26 | Distributed binaries under MacOS are signed. | Pierre Boutillier | |
| 2014-08-26 | Configure.ml creates metadata to annotate MacOS binaries | Pierre Boutillier | |
| 2014-08-26 | Debug RAKAM | Pierre Boutillier | |
| 2014-08-26 | sed s'/_one_var/_on/g' | Jason Gross | |
| For consistency with ChoiceFacts | |||
| 2014-08-26 | Generalize EqdepFacts | Jason Gross | |
| The generalized versions are names *_one_var. We preserve backwards compatibility by defining the old versions in terms of the generalized ones. This closes the rest of Bug 3019, and closes pull request #6. | |||
| 2014-08-26 | Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors in | Matthieu Sozeau | |
| stm test-suite files. | |||
| 2014-08-26 | Make evarconv and unification able to handle eta for records in presence | Matthieu Sozeau | |
| of metas/evars | |||
| 2014-08-26 | Fix compilation error due to commented code in previous commit by Hugo. | Matthieu Sozeau | |
| 2014-08-25 | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau | |
| to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing. | |||
| 2014-08-25 | Fix computation of dangling constraints at the end of a proof (bug #3531). | Matthieu Sozeau | |
| 2014-08-25 | Fixing the essence of naming bug #3204: use same strategy for naming | Hugo Herbelin | |
| cases pattern variables than for naming forall/fun binders (but still avoiding constructor names). Note in passing: such as it is implemented, the general strategy is in O(n²) in the number of nested binders, because, when computing the name for each 'fun x => c" (or forall, or a pattern name), the names from the outside c and visibly occurring in c are computed. | |||
| 2014-08-25 | Add an is_cofix tactic | Jason Gross | |
| Should we also add is_* tactics for other things? is_rel, is_meta, is_sort, is_cast, is_prod, is_lambda, is_letin, is_app, is_const, is_ind, is_constructor, is_case, is_proj? | |||
| 2014-08-25 | Prerequisite to fix stm test-suite when not in -local | Pierre Boutillier | |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross | |
| It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar). | |||
| 2014-08-25 | instanciation is French, instantiation is English | Jason Gross | |
| 2014-08-25 | Clean up a comment in plugins/romega/ReflOmegaCore | Jason Gross | |
| Based on suggestion by @gasche. | |||
| 2014-08-25 | Grammar: "avoiding to" isn't proper, either | Jason Gross | |
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross | |
| I'm not quite sure why, but I'm pretty sure it's not. Rather, in "allowing for foo" and "allowing to foo", "foo" modifies the sense in which someting is allowed, rather than it being "foo" that's allowed. "Allowing fooing" generally works, though it can sound a bit awkward. "Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always acceptable, in-as-much as it's ok to use "one". I haven't touched the older instances of it in the CHANGES file. | |||
| 2014-08-25 | Correct a spelling mistake | Jason Gross | |
| 2014-08-25 | factored out require_modifiers + bug fix. | Gregory Malecha | |
| Conflicts: tools/coqdep_lexer.mll | |||
| 2014-08-25 | coqdep comments counter is in the stack | Pierre Boutillier | |
| 2014-08-25 | a comment about the new state. | Gregory Malecha | |
| 2014-08-25 | Support for Timeout n and From .. | Gregory Malecha | |
| - The state machine gets kind of complex maybe it should become a parser at some point? | |||
| 2014-08-25 | Make coqdep find Require commands prefixed by Time | Gregory Malecha | |
| 2014-08-25 | Fixing previous commit. | Pierre-Marie Pédrot | |
| 2014-08-25 | Fixing a bug introduced in the extension of 'apply in' + simplifying code. | Hugo Herbelin | |
| 2014-08-24 | Removing a unused legacy parsing rule. | Pierre-Marie Pédrot | |
| 2014-08-24 | Fixing bug #3404. | Pierre-Marie Pédrot | |
| 2014-08-24 | Enabling drag & drop on the source view widgets. | Pierre-Marie Pédrot | |
| Sort of fixes bug #2765, but the file loading is broken and puts coqtop in an inconsistent state, so that even the previous half-working patch was actually not functionning at all. This should be fixed eventually. | |||
| 2014-08-23 | Tactics.is_quantified_hypothesis does not reduce anymore to decide whether | Pierre-Marie Pédrot | |
| a variable is quantified in the goal. This is only used by induction, and it should be a bad practice to depend on an invisible binder. | |||
| 2014-08-23 | Fix test-suite file. | Matthieu Sozeau | |
| 2014-08-23 | Fixing ml-dot & mli-dot targets. | Pierre-Marie Pédrot | |
| 2014-08-23 | Fixing bug #3533. | Pierre-Marie Pédrot | |
| Now error printing tries to set universe printing when two terms are not desambiguated. | |||
| 2014-08-23 | Tactics.unify in the new monad. | Pierre-Marie Pédrot | |
| 2014-08-22 | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau | |
| 2014-08-21 | Removing unused parts of the Goal.sensitive monad. | Pierre-Marie Pédrot | |
| Some legacy code remains to keep the newish refine tactic working, but ultimately it should be removed. I did not manage to do it properly though, i.e. without breaking the test-suite furthermore. | |||
| 2014-08-21 | Removing a Goal.sensitive in Rewrite. | Pierre-Marie Pédrot | |
| 2014-08-21 | Removing a use of tclSENSITIVE in Rewrite. | Pierre-Marie Pédrot | |
| 2014-08-21 | Removing a use of tclSENSITIVE in Rewrite. | Pierre-Marie Pédrot | |
| 2014-08-21 | Removing a use of tclSENSITIVE in Rewrite. | Pierre-Marie Pédrot | |
| 2014-08-21 | Improve consistency of whitespace (beautifier). | Xavier Clerc | |
| 2014-08-21 | Improve consistency of whitespace (beautifier). | Xavier Clerc | |
| 2014-08-21 | Space after [identity] coercion keywords (beautifier). | Xavier Clerc | |
| 2014-08-21 | Avoid redundant spaces (beautifier). | Xavier Clerc | |
| 2014-08-21 | Do not drop the locality qualifier (beautifier). | Xavier Clerc | |
| 2014-08-21 | Make beautify-archive usable on non-GNU systems. | Xavier Clerc | |
| 2014-08-19 | Removing a use of Goal.refine. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |