| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | 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-21 |
| | | |||
| * | 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-19 |
| | | |||
| * | Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was ↵ |  Matthieu Sozeau | 2014-08-18 |
| | | | | | larger than Type.1 etc... | ||
| * | 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 | 2014-08-18 |
| | | | | | | | | 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. | ||
| * | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin | 2014-08-18 |
| | | | | | "pat/term" for "apply term on current_hyp as pat". | ||
| * | Improving error message when applying rewrite to an expression which is not ↵ | Hugo Herbelin | 2014-08-18 |
| | | | | | an equality. | ||
| * | Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to | Hugo Herbelin | 2014-08-18 |
| | | | | | | | | | | | | 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). | ||
| * | 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 | 2014-08-18 |
| | | | | | Isolating a core tactic in replace, shareable to cutrewrite. | ||
| * | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin | 2014-08-18 |
| | | | | | | scheme, redundancies, possibility of chaining a tactic knowing the name of introduced hypothesis, new proof engine). | ||
| * | Spotted a source of failure of the constr printer in debugger. | Hugo Herbelin | 2014-08-18 |
| | | |||
| * | Reorganisation of intropattern code | Hugo Herbelin | 2014-08-18 |
| | | | | | | | | | | | | | | | | | - 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? | ||
| * | Reorganization of tactics: | Hugo Herbelin | 2014-08-18 |
| | | | | | | | | | | - 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) | ||
| * | 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 | 2014-08-18 |
| | | | | | | | unsatisfiable constraint failures but give sensible error messages if an occurrence was found and only typeclass resolution failed. Fixes MathClasses. | ||
| * | Fix test-suite file. | Matthieu Sozeau | 2014-08-18 |
| | | |||
| * | Fixing include of debugger. | Pierre-Marie Pédrot | 2014-08-18 |
| | | |||
| * | Moving the TacAlias node out of atomic tactics. | Pierre-Marie Pédrot | 2014-08-18 |
| | | |||
| * | Moving the TacExtend node from atomic to plain tactics. | Pierre-Marie Pédrot | 2014-08-18 |
| | | | | | | Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values. | ||
| * | Removing documentation related to the deprecated State machinery. | Pierre-Marie Pédrot | 2014-08-16 |
| | | |||
| * | Better printing of Ltac values. | Pierre-Marie Pédrot | 2014-08-16 |
| | | |||
| * | Fixing too restrictive detection of resolution of evars in "apply in" | Hugo Herbelin | 2014-08-16 |
| | | | | | (revealed by contribution PTSF). | ||
| * | More self-contained code for tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-15 |
| | | |||
| * | Removing unused Refiner.tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-15 |
| | | |||
| * | Remove confusing behavior of unify_with_subterm that could fail with | Matthieu Sozeau | 2014-08-14 |
| | | | | | | | | NoOccurenceFound when only typeclass resolution failed. Might break some scripts relying on backtracking on typeclass resolution failures to find other terms to rewrite, which can be fixed using occurrences or directly setoid_rewrite. | ||
| * | Fix program using an the unsubstituted type of the original obligation | Matthieu Sozeau | 2014-08-14 |
| | | | | | instead of the normalized one at the end of the proof. Fixes bug #3517. | ||
| * | Fix non-printing of coercions for primitive projections (fixes bug #3433). | Matthieu Sozeau | 2014-08-14 |
| | | |||
| * | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau | 2014-08-14 |
| | | |||
| * | Restore the error-handling behavior of [change], which was silently failing | Matthieu Sozeau | 2014-08-14 |
| | | | | | when conversion in the goal failed. | ||
| * | Fix elimschemes accessing directly the universe context of inductives (fixes ↵ | Matthieu Sozeau | 2014-08-14 |
| | | | | | | | test-suite file HoTT_coq_089.v). | ||
| * | Fix test-suite files according to new parsing rule for application of primitive | Matthieu Sozeau | 2014-08-13 |
| | | | | | projections. | ||
| * | Small optimization in Cooking: do not construct identity substitutions. | Pierre-Marie Pédrot | 2014-08-13 |
| | | |||
| * | Bettre pretty-printing of evar maps, avoids printing universe information | Matthieu Sozeau | 2014-08-13 |
| | | | | | for typeclass errors. | ||
| * | Upgrading output tests. | Hugo Herbelin | 2014-08-12 |
| | | | | | | | | | | | | | output/Arguments.v output/ArgumentsScope.v output/Arguments_renaming.v output/Cases.v output/Implicit.v output/PrintInfos.v output/TranspModType.v Main changes: monomorphic -> not universe polymorphic, Peano vs Nat | ||
| * | Bug #3469: fixing unterminated comment. | Hugo Herbelin | 2014-08-12 |
| | | |||
| * | In bug #2406, renouncing to test failure of parsing error. | Hugo Herbelin | 2014-08-12 |
| | | | | | | (AFAIU, it is the table of supported unicode characters which has to be upgraded anyway.) | ||
| * | Quick fix for avoiding infinitely many respawning and Warning "Coq | Hugo Herbelin | 2014-08-12 |
| | | | | | died" when coqtop or coqtopide.cmxs are in inconsistent state. | ||
| * | Fixing parsing of bullets after a "...". | Hugo Herbelin | 2014-08-12 |
| | | | | | | | | | | | | | | | The lexer parses bullets only at the beginning of sentence. In particular, the lexer recognizes sentences (this feature was introduced for the translator and it is still used for the beautifier). It recognized "." but not "...'. I added "..." followed by space or eol as a terminator of sentences. I hope this is compatible with the rest of the code dealing with end of sentences. Fixed also parse_to_dot which was not aware of "...". Maybe there are similar things to do with coqide or PG? | ||
| * | A couple of fixes/improvements in -beautify, but backtracking on | Hugo Herbelin | 2014-08-12 |
| | | | | | change of printing format of forall (need more thinking). | ||
| * | Fix bug introduced by earlier commit on first-order unification of primitive |  Matthieu Sozeau | 2014-08-10 |
| | | | | | | projections and their expansion, allowing unfolding when it fails. Cleanup code in reductionops.ml | ||
| * | Fix unification which was failing when unifying a primitive projection against | Matthieu Sozeau | 2014-08-09 |
| | | | | | its expansion if it could reduce (fixes bug #3480). | ||
| * | Allow pattern matching on the applied form of projections with primitive | Matthieu Sozeau | 2014-08-09 |
| | | | | | applications, solving part of bug #3503. | ||
| * | Do early occur-check in unification to allow eta to fire (fixes bug #3477) | Matthieu Sozeau | 2014-08-09 |
| | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |