| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-07-10 | Native compiler: make non-fatal linking errors silent except in debug mode. | Maxime Dénès | |
| 2015-07-10 | Native compiler: refactor code handling pre-computed values. | Maxime Dénès | |
| Fixes #4139 (Not_found exception with Require in modules). | |||
| 2015-07-09 | Kernel/Checker: Cleanup fixes of substitutions due to let-ins. | Matthieu Sozeau | |
| Avoid undeeded large substitutions, and add test-suite file for fixed bug 4283 in closed/ | |||
| 2015-07-09 | Kernel: primitive projections handling of let-ins | Matthieu Sozeau | |
| Fixes bug #4176 (actually two bugs in one) Correct computation of the type of primitive projections in presence of let-ins. | |||
| 2015-07-09 | Improve semantics of -native-compiler flag. | Maxime Dénès | |
| Since Guillaume's, launching coqtop without -native-compiler and call native_compute would mean recompiling silently all dependencies, even if they had been precompiled (e.g. the stdlib). The new semantics is that -native-compiler disables separate compilation of the current library, but still tries to load precompiled dependencies. If loading fails when the flag is on, coqtop stays silent. | |||
| 2015-07-09 | Template polymorphism: A bug-fix for Bug #4258 | mlasson | |
| Reviewed by M. Sozeau This commit fixes template polymorphism and makes it more precise, applying to non-linear uses of the same universe in parameters of template-polymorphic inductives. See bug report and https://github.com/coq/coq/pull/69 for full details. I also removed some deadcode in checker/inductive.ml. I do not know if it is also necessary to fix checker/indtypes.ml. | |||
| 2015-07-09 | Make retyping of projections more resilient to wrong environment. | Maxime Dénès | |
| Unfortunately, it seems that retyping can be called in ill-typed terms and/or in the wrong environment. This was broken for projections by my commit a51cce369b9c634a93120092d4c7685a242d55b1 | |||
| 2015-07-09 | Fixing printing of primitive coinductive record status. | Pierre-Marie Pédrot | |
| They do not have eta-rule indeed, even though it was displayed as such. | |||
| 2015-07-08 | Ide: fix bug #4284 for good | Matthieu Sozeau | |
| Correct folding order over the named_list_context. | |||
| 2015-07-08 | Bug 4284: Tentative bugfix for detyping exception. | Matthieu Sozeau | |
| 2015-07-08 | Checker: Report bugfixes from kernel/inductive.ml | Matthieu Sozeau | |
| Wrong handling of mind_params_ctxt... | |||
| 2015-07-08 | Fix documentation of universes. | Matthieu Sozeau | |
| 2015-07-08 | Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262) | Guillaume Melquiond | |
| 2015-07-08 | Fix command-line documentation of coq-tex. | Guillaume Melquiond | |
| 2015-07-08 | Fix documentation. | Guillaume Melquiond | |
| 2015-07-08 | Use the same optimization level for the VM, whatever the debug level. | Guillaume Melquiond | |
| 2015-07-07 | Document Set/Print Firstorder Solver option. | Matthieu Sozeau | |
| 2015-07-07 | Checker: Fix bug #4282 | Matthieu Sozeau | |
| Adapt to new [projection] abstract type comprising a constant and a boolean. | |||
| 2015-07-07 | Univs: bug fix. | Matthieu Sozeau | |
| Missing universe substitutions of mind_params_ctxt when typechecking cases, which appeared only when let-ins were used. | |||
| 2015-07-07 | test-suite: Fix test-suite Makefile | Matthieu Sozeau | |
| Using relative path for coqlib, for some reason this fails on Mac OS X. Took the easiest way to fix it. | |||
| 2015-07-07 | Univs/minimization: Fix unused variable bug. | Matthieu Sozeau | |
| 2015-07-07 | Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its | Hugo Herbelin | |
| verbose flag. | |||
| 2015-07-06 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-07-06 | Temporarily disable test file for #3922. | Maxime Dénès | |
| 2015-07-06 | Test case for #4203, fixed by commit a51cce36. | Maxime Dénès | |
| 2015-07-05 | Fixing documentation (see Maxime's mail on coqdev, July 3). | Hugo Herbelin | |
| 2015-07-05 | More precise rewording about asymmetric patterns. | Hugo Herbelin | |
| 2015-07-05 | Fix handling of primitive projections in VM. | Maxime Dénès | |
| I'm pushing this patch now because the previous treatment of such projections in the VM was already unsound. It should however be carefully reviewed. | |||
| 2015-07-03 | Fixing bug #4265: coqdep does not handle From ... Require. | Pierre-Marie Pédrot | |
| The search algorithm is not satisfactory though, as it crawls through all known files to find the proper one. We should rather use some trie-based data structure, but I'll leave this for a future commit. | |||
| 2015-07-03 | Fix convertibility of primitive projections for native_compute. | Maxime Dénès | |
| Stuck primitive projections were never convertible. | |||
| 2015-07-02 | Remove a line from test-suite. | Maxime Dénès | |
| Triggers a bug in declarative mode. Waiting for someone to volunteer and fix the bug, but meanwhile I'm trying to fix the test-suite. | |||
| 2015-07-02 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-07-02 | More robust pattern matching on structured constants in VM. | Maxime Dénès | |
| 2015-07-02 | Revert "Add target to install dev files." | Maxime Dénès | |
| Broke the build. This reverts commit ef6459b00999a29183edc09de9035795ff7912e9. | |||
| 2015-07-02 | Fix loop in assumptions (Close: #4275) | Enrico Tassi | |
| 2015-07-02 | Display functions for primitive projections. | Maxime Dénès | |
| 2015-07-01 | Further simplification of the graph traversal in Univ. | Pierre-Marie Pédrot | |
| We passed the arc to be marked as visited to the functions pushing the neighbours on the remaining stack, but this can be actually done before pushing them, as the [process_le] and [process_lt] functions do not rely on the visited flag. This exposes more clearly the invariants of the algorithm. | |||
| 2015-07-01 | Notation: use same level for "@" in constr: and pattern: (Close: #4272) | Enrico Tassi | |
| A possible script breakage can occur if one has a notation at level 11 that is also right associative (now 11 is left associative). Thanks Georges for debugging that. | |||
| 2015-06-30 | Removing dead code in coqdep. | Pierre-Marie Pédrot | |
| Since commit 2f521670fbd, the Require "file" syntax was not used anymore by coqtop but the code handling it was still there in coqdep. We finish the work by erasing the remnant code. | |||
| 2015-06-30 | Another missing Fail and comment in test-suite. | Maxime Dénès | |
| 2015-06-30 | Missing "Fail" in test-suite. | Maxime Dénès | |
| 2015-06-29 | Assumptions: more informative print for False axiom (Close: #4054) | Enrico Tassi | |
| When an axiom of an empty type is matched in order to inhabit a type, do print that type (as if each use of that axiom was a distinct foo_subproof). E.g. Lemma w : True. Proof. case demon. Qed. Lemma x y : y = 0 /\ True /\ forall w, w = y. Proof. split. case demon. split; [ exact w | case demon ]. Qed. Print Assumptions x. Prints: Axioms: demon : False used in x to prove: forall w : nat, w = y used in w to prove: True used in x to prove: y = 0 | |||
| 2015-06-29 | class_tactics: make interruptible | Enrico Tassi | |
| Tracing with gdb by Alec Faithfull | |||
| 2015-06-29 | class_tactics: remove catch-all, use Errors.noncritical | Enrico Tassi | |
| 2015-06-29 | win: compile with -debug | Enrico Tassi | |
| 2015-06-29 | Fix test file for #4214 which was fixed by Hugo. | Maxime Dénès | |
| 2015-06-29 | Better test case by PMP for #3948. | Maxime Dénès | |
| 2015-06-29 | Code documentation of the TACTIC/VERNAC EXTEND macros. | Pierre-Marie Pédrot | |
| 2015-06-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-28 | Fix incompleteness of conversion used by evarconv | Matthieu Sozeau | |
| In case we need to backtrack on universe inconsistencies when converting two (incompatible) instances of the same constant and unfold them. Bug reported by Amin Timany. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |