| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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). | |||
| 2014-08-18 | Spotted a source of failure of the constr printer in debugger. | Hugo Herbelin | |
| 2014-08-18 | Reorganisation of intropattern code | Hugo Herbelin | |
| - emphasizing the different kinds of patterns - factorizing code of the non-naming intro-patterns Still some questions: - Should -> and <- apply to hypotheses or not (currently they apply to hypotheses either when used in assert-style tactics or apply in, or when the term to rewrite is a variable, in which case "subst" is applied)? - Should "subst" be used when the -> or <- rewrites an equation x=t posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)? - Should -> and <- be applicable in non assert-style if the lemma has quantifications? | |||
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin | |
| - made "apply" tactics of type Proofview.tactic, as well as other inner functions about elim and assert - used same hypothesis naming policy for intros and internal_cut (towards a reorganization of intro patterns) - "apply ... in H as pat" now supports any kind of introduction pattern (doc not changed) | |||
| 2014-08-18 | Fix test-suite file. | Matthieu Sozeau | |
| 2014-08-18 | Fix test-suite files. | Matthieu Sozeau | |
| 2014-08-18 | Refine patch for behavior of unify_to_subterm to allow backtracking on | Matthieu Sozeau | |
| unsatisfiable constraint failures but give sensible error messages if an occurrence was found and only typeclass resolution failed. Fixes MathClasses. | |||
| 2014-08-18 | Fix test-suite file. | Matthieu Sozeau | |
| 2014-08-18 | Fixing include of debugger. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |