| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-29 | Fixes #7110 ("as" untested while looking for notation for nested patterns). | Hugo Herbelin | |
| 2018-03-29 | [Sphinx] Add chapter 26 | Maxime Dénès | |
| Thanks to Paul Steckler for porting this chapter. | |||
| 2018-03-29 | [Sphinx] Move chapter 26 to new infrastructure | Maxime Dénès | |
| 2018-03-29 | Fix #6770: fixpoint loses locality info in proof mode. | Gaëtan Gilbert | |
| 2018-03-29 | Fix #6631: Derive Plugin gives "Anomaly: more than one statement". | Pierre-Marie Pédrot | |
| We use a lower level function that accesses the proof without raising an anomaly. This is a direct candidate for backport, so I used a V82 API but eventually this API should be cleaned up. | |||
| 2018-03-29 | [Sphinx] Add chapter 24 | Maxime Dénès | |
| Thanks to Matthieu Sozeau for porting this chapter. | |||
| 2018-03-29 | [Sphinx] Move chapter 24 to new infrastructure | Maxime Dénès | |
| 2018-03-29 | [Sphinx] Add chapter 23 | Maxime Dénès | |
| Thanks to Pierre Letouzey for porting this chapter. | |||
| 2018-03-29 | [Sphinx] Move chapter 23 to new infrastructure | Maxime Dénès | |
| 2018-03-29 | [Sphinx] Remove duplicate entry for command `Coercion` | Maxime Dénès | |
| 2018-03-29 | [Sphinx] Add chapter 18 | Maxime Dénès | |
| Thanks to Pierre Letouzey for porting this chapter. | |||
| 2018-03-29 | [Sphinx] Move chapter 18 to new infrastructure | Maxime Dénès | |
| 2018-03-29 | Merge PR #7057: Sphinx Chapter 20: Type Classes | Maxime Dénès | |
| 2018-03-29 | Merge PR #7072: Update codeowners | Maxime Dénès | |
| 2018-03-29 | Remove dev/doc/changes.md from files with a code owner. | Théo Zimmermann | |
| Like CHANGES, and the test-suite folder, this file receives too many updates to have a code owner. It is the job of the reviewer of the PR to review changes to these files as well. | |||
| 2018-03-29 | Preparing old-style refine from logic.ml to deal with "Cases" proof | Hugo Herbelin | |
| terms whose branches are in eta-let-expanded canonical form. This is a hack intended to work only with destruct/case as they are currently implemented. Would not work with arbitrary proofs of the form "Cases(ci,p,c,[|...;b;...|] given to logic.ml for which b, if with Metas, has not the form of an eta-let-expanded Meta. | |||
| 2018-03-28 | Supporting fix/cofix in Ltac pattern-matching (wish #7092). | Hugo Herbelin | |
| This is done by not failing for fix/cofix while translating from glob_constr to constr_pattern. | |||
| 2018-03-28 | Patterns: Accepting patterns in PFix and PCofix and not only constr. | Hugo Herbelin | |
| 2018-03-28 | Adding Array.fold_left4. | Hugo Herbelin | |
| 2018-03-28 | Detyping: Adding a variant of share_names for patterns. | Hugo Herbelin | |
| 2018-03-28 | Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1). | Hugo Herbelin | |
| 2018-03-28 | Patternops: renaming an internal function to more closely match its effect. | Hugo Herbelin | |
| 2018-03-28 | Glob_ops: cosmetic renaming to reflect the type of objects. | Hugo Herbelin | |
| 2018-03-28 | Getting rid of some false "collision between bound variable names" warnings. | Hugo Herbelin | |
| - In a situation like "match x with ... end" with no "return" clause we don't warn for the implicit "as x" coming from repeating "x" - In a multiple fixpoint, we don't warn for the recursive context being distributed several times over the different mutual components. | |||
| 2018-03-28 | Fix #7101: STM delegation policy broken | Maxime Dénès | |
| I make here a minimal fix, but a lot of cleaning should be done around Aux_file handling, including removing some code from the kernel. | |||
| 2018-03-28 | [api] Deprecate a couple of aliases that we missed. | Emilio Jesus Gallego Arias | |
| 2018-03-28 | Merge PR #7090: stm: don't propagate side effects when editing a proof | Emilio Jesus Gallego Arias | |
| 2018-03-28 | coqide: avoid marking sentences that are not in the document anymore | Enrico Tassi | |
| 2018-03-28 | Merge PR #6961: [test-suite] Add backtracking test for `Load`. | Enrico Tassi | |
| 2018-03-27 | stm: don't propagate side effects when editing a proof | Enrico Tassi | |
| 2018-03-27 | Adding tacticals tclBINDFIRST/tclBINDLAST. | Hugo Herbelin | |
| Design choice: Failing with an anomaly or with a catchable Ltac error "Fail": we fail with a Fail as it was the case with the related constrained version of tclTHENFIRST/tclTHENLAST. | |||
| 2018-03-27 | Export Proofview.undefined as "unsafe" primitive. | Hugo Herbelin | |
| 2018-03-27 | Adding informative variant of shelve_unifiable returning set of shelved evars. | Hugo Herbelin | |
| 2018-03-27 | Congruence: Fixing a bug with native projections. | Hugo Herbelin | |
| There is a code to turn constants denoting projections into proper primitive projections, but it did not drop parameters. The code seems anyway redundant with an "expand_projections" which is already present in Cctac.decompose_term. After removal of this code, the two calls to congruence added to cc.v work. | |||
| 2018-03-27 | Congruence: typography in a comment. | Hugo Herbelin | |
| 2018-03-27 | Congruence: getting rid of a detour by the compatibility layer of proof engine. | Hugo Herbelin | |
| The V82 compatibility layer of the proof engine was used by cc (congruence closure) for the sole purpose of maintaining an environment and a sigma. We inline the corresponding env and sigma in the state of cc algorithm to get rid of the compatibility layer. | |||
| 2018-03-27 | [default.nix] Unpin nixpkgs | Maxime Dénès | |
| Sphinx dependencies are now available in unstable channel | |||
| 2018-03-27 | Merge PR #6835: Deprecate undocumented "intros until 0" in favor of "intros *" | Pierre-Marie Pédrot | |
| 2018-03-27 | Merge PR #7062: Slightly refining some error messages about unresolvable evars. | Pierre-Marie Pédrot | |
| 2018-03-27 | Expliciting and taking advantage of a representation invariant in Esubst. | Pierre-Marie Pédrot | |
| 2018-03-27 | Adding a fiat-parser overlay | Hugo Herbelin | |
| 2018-03-27 | Fixing #5547 (typability of return predicate in nested pattern-matching). | Hugo Herbelin | |
| Answering to commit about #5500: we don't know in general if the return predicate T(y1,..,yn,x) in the intermediate step of a nested pattern-matching is a sort, but we don't even know if it is well-typed: retyping is not enough, we need full typing. | |||
| 2018-03-27 | Fixing #5500 (missing test in return clause of match leading to anomaly). | Hugo Herbelin | |
| This is a quick fix to check in nested pattern-matching that the return clause is typed by an arity (there was already a check when the return clause was given explicitly - in the 3rd section of prepare_predicate -; it was automatically typed by a sort when the return clause was coming by pattern-matching with the type constraint, since the type constraint is a type; but it was not done when the predicate was derived from a former predicate in nested pattern-matching). Indeed, in nested pattern-matching, we know that the return predicate has the form λy1..yn.λx:I(y1,..,yn).T(y1,..,yn,x) and we know that T(v1,...,vn,u) : Type for the effective u:I(v1,..,vn) we are matching on, but we don't know if T(y1,..,yn,x) is itself a sort (e.g. it can be a "match" which reduces to a sort when instantiated with v1..vn, but whose evaluation remains blocked when the y1..yn are variables). Note that in the bug report, the incorrect typing is produced by small inversion. In practice, we can raise the anomaly also without small inversion, so we fix it in the general case. See file 5500.v for details. | |||
| 2018-03-27 | Fix printing of toplevel record values. | Pierre-Marie Pédrot | |
| 2018-03-27 | Fixup strict mode for patterns | Pierre-Marie Pédrot | |
| 2018-03-26 | Fixes #7011 (Fix/CoFix were not considered in tactic unification). | Hugo Herbelin | |
| 2018-03-26 | [doc] Port Chapter 20 Type Classes to Sphinx | Matthieu Sozeau | |
| 2018-03-26 | Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes ↵ | Maxime Dénès | |
| AppVeyor fail. | |||
| 2018-03-26 | Move Classes.tex to type-classes.rst | Matthieu Sozeau | |
| 2018-03-26 | Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer. | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |