| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-08-19 | New primitive allowing to modify refine handles. | Pierre-Marie Pédrot | |
| 2014-08-18 | Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was ↵ | Matthieu Sozeau | |
| larger than Type.1 etc... | |||
| 2014-08-18 | Fixing unification of subterms identified by patterns. | Hugo Herbelin | |
| 2014-08-18 | Lazy interpretation of patterns so that expressions such as "intros H H'/H" | Hugo Herbelin | |
| can be given with second H bound by the first one. Not very satisfied by passing closure to tactics.ml, but otherwise tactics would have to be aware of glob_constr. | |||
| 2014-08-18 | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin | |
| "pat/term" for "apply term on current_hyp as pat". | |||
| 2014-08-18 | Improving error message when applying rewrite to an expression which is not ↵ | Hugo Herbelin | |
| an equality. | |||
| 2014-08-18 | Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to | Hugo Herbelin | |
| integrate to "rewrite"?) with the code of "replace". Incidentally, "inversion" relies on dependent rewrite, with an incompatibility introduced. Left-to-right rewriting is now done with "eq_rec_r" while before it was done using "eq_rec" of "eq_sym". The first one reduces to the second one but simpl is not anymore able to reduce "eq_rec_r eq_refl". Hopefully cbn is able to do it (see Zdigits). | |||
| 2014-08-18 | A few more comments in tactics.mli and hippatern.ml. | Hugo Herbelin | |
| 2014-08-18 | Slight simplification of naming of tactics in equality.ml (hopefully). | Hugo Herbelin | |
| Isolating a core tactic in replace, shareable to cutrewrite. | |||
| 2014-08-18 | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin | |
| scheme, redundancies, possibility of chaining a tactic knowing the name of introduced hypothesis, new proof engine). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |