| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Update copyright headers. |  Maxime Dénès | 2016-01-20 |
| | | |||
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| | | |||
| * | 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". | ||
| * | 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? | ||
| * | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code |  Pierre Letouzey | 2014-03-02 |
| NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |