| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-07 | Avoid a warning with Meta's names in debugger. | Hugo Herbelin | |
| 2014-10-07 | coq_makefile: explicit target install-toploop for toploop plugins | Enrico Tassi | |
| 2014-10-06 | Make tclEFFECTS also update the env in the proof monad | Enrico Tassi | |
| 2014-10-06 | fix wrong escaping in coq_makefile | Enrico Tassi | |
| 2014-10-06 | decl_mode: stay in declarative mode | Enrico Tassi | |
| This solution is a bit dumb, but I guess does what one expects. Each decl mode proof commands stays in proof mode. | |||
| 2014-10-05 | Semantic fix of a refine in Rewrite. | Pierre-Marie Pédrot | |
| This code was wrong but luckily unused. It instantiated an evar with an instance where the let-in bindings were removed. | |||
| 2014-10-05 | Check compatibility of types in change depending on whether it is a | Hugo Herbelin | |
| term or a type. Continuation of 9a82982c1eb. | |||
| 2014-10-05 | A few improvements on pattern-matching compilation. | Hugo Herbelin | |
| - Optimize the removal of generalization when there is no dependency in the generalized variable (see postprocess_dependencies, and the removal of dependencies in the default type of impossible cases). - Compute the onlydflt flag correctly (what allows automatic treatment of impossible cases even when there is no clause at all). | |||
| 2014-10-04 | A few Global.env removed. | Hugo Herbelin | |
| 2014-10-03 | Fixing #3193 (honoring implicit arguments in local definitions). | Hugo Herbelin | |
| 2014-10-03 | Classify segfaults as failures in opened bugs. | Xavier Clerc | |
| 2014-10-03 | Classify segfaults as failures in opened bugs | Xavier Clerc | |
| 2014-10-03 | Fixing #3606 continued (doc of Scheme Boolean Equality Scheme). | Hugo Herbelin | |
| 2014-10-03 | Removing deactivated command Show Tree. | Hugo Herbelin | |
| 2014-10-03 | Fixing #3657 (check that both sides of a "change with" have the same | Hugo Herbelin | |
| type, what is necessary condition to ensure that the conversion of bodies will not raise an anomaly). | |||
| 2014-10-03 | Test for bug #3652 fixed in 0fb36157b9ba | Hugo Herbelin | |
| 2014-10-03 | Fixing ennoying warning about evars named ?23 and so on. | Hugo Herbelin | |
| 2014-10-03 | Fixing #3623 (unbound evars in types in a call to "change with"). | Hugo Herbelin | |
| 2014-10-03 | Add a bunch of reproduction files for bugs. | Xavier Clerc | |
| 2014-10-03 | Fixing #3634 (wrong env in "cannot instantiate because not in its | Hugo Herbelin | |
| scope" error message). | |||
| 2014-10-03 | Adapting output/Arguments_renaming continued. | Hugo Herbelin | |
| 2014-10-02 | Implement module subtyping for polymorphic constants (errors on | Matthieu Sozeau | |
| inductives). The implementation constant should have the a universe instance of the same length, we assume the universes are in the same order and we check that the definition does not add any constraints to the expected ones. This fixes bug #3670. | |||
| 2014-10-02 | Fixing interpretation of constr under binders which was broken after | Hugo Herbelin | |
| it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). | |||
| 2014-10-02 | Fixing bug #2810 (autounfold on local variable declared as hint but cleared). | Hugo Herbelin | |
| 2014-10-02 | Completing fixing order of parameters when translating from | Hugo Herbelin | |
| glob_constr to constr_pattern. Was partially fixed to solve #3088 (8e88b7adab) in but the order of lambdas was still incorrect as the fix of the order of lambdas in second-order pattern-matching for #3136 showed (83159124ce22). | |||
| 2014-10-02 | An evar name changed in output test. | Hugo Herbelin | |
| 2014-10-02 | Adapting the output test Notations: | Hugo Herbelin | |
| - unbound variables in notation are allowed, forcing only parsing mode - plus and mult are now themselves abbreviations - evars are named | |||
| 2014-10-02 | Added make dependency in %.out in output tests. | Hugo Herbelin | |
| 2014-10-02 | Revert "test-suite: New names for vars but the expected invariant is preserved" | Hugo Herbelin | |
| This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf. Going back to the convention of naming bound variables in hypotheses of the goal as in 8.4. My arguments for the revert are: - apply ... with (id:=...) would have to be changed too, then possibly breaking the compatibility - the naming became dependent of the order of variables as in x:nat H:forall x0, x0=0 ===== goal but H:forall x, x=0 x:nat ===== goal Accordingly, this is all a matter of convention, since the meaning of bindings is anyway the same in both cases. | |||
| 2014-10-02 | Adapting output/Arguments_renaming.out after fixing printing of | Hugo Herbelin | |
| constants which without a @ would have a maximally inserted implicit argument. | |||
| 2014-10-02 | Print type and environment of unsolved holes. | Arnaud Spiwack | |
| Was just printed in the case of internal holes. Also: replace [str] by [strbrk] in error message of unsolved holes for better layout. | |||
| 2014-10-02 | Work around issues with FO unification trying to unify terms of | Matthieu Sozeau | |
| potentially different types, resulting in ill-typed terms due to eta. Projection expansion now fails gracefully on retyping errors. The proper fix to unification, checking that the heads for FO have unifiable types, is currently too strong, adding unnecessary universe constraints, so it is disabled for now. It might be quite expensive too also it's not noticeable on the stdlib. | |||
| 2014-10-02 | Move eta-expansion after delta reduction in kernel reduction. This makes | Matthieu Sozeau | |
| it closer to evarconv/unification's behavior and it is less prone to weird failures and successes in case of first-order unification sending problems where the two terms have different types. | |||
| 2014-10-02 | Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv. | Matthieu Sozeau | |
| 2014-10-01 | eta contractions | Pierre Boutillier | |
| 2014-10-01 | argument flip of Cyclic31.nshiftr and Cyclic31.nshiftl | Pierre Boutillier | |
| 2014-10-01 | Simpl less (so that cbn will not simpl too much) | Pierre Boutillier | |
| 2014-10-01 | Fix cbn behavior wrt simpl no match | Pierre Boutillier | |
| 2014-10-01 | Fix the refolding by cbn of mutal constants defined in not included modules | Pierre Boutillier | |
| 2014-10-01 | Fixing nice printing of error reporting with ml tactics bound to ltac names. | Hugo Herbelin | |
| 2014-10-01 | Made Tacsubst independent of Auto at linking time so that Tacenv does | Hugo Herbelin | |
| not draw Auto. | |||
| 2014-10-01 | Going back on granting wish #1039 in f5d7b2b1e so that apply with | Hugo Herbelin | |
| works correctly with an hypothesis of the context and knowing that related bug #3204 had its own fix. | |||
| 2014-10-01 | Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evars | Hugo Herbelin | |
| by names): VarInstance behaves like GoalEvar for type class resolution. | |||
| 2014-10-01 | Fixing use of arguments renaming in apply which was broken after | Hugo Herbelin | |
| reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f: using renaming also in retyping. | |||
| 2014-10-01 | Updating to the new use of 3 universes, after Hurkens is simplified. | Hugo Herbelin | |
| 2014-10-01 | STM: report the (structured) goals as XML | Carst Tankink | |
| The leafs of the XML trees are still pretty-printed strings, but this could be refined later on. | |||
| 2014-10-01 | Factored out IDE goal structure. | Carst Tankink | |
| The more structured goal record type of CoqIDE is also useful for other interfaces (in particular, for PIDE). To support this, the datatype was factored out to the Proof module. In addition, the record gains a type parameter, to allow interfaces to adapt the output to their needs. To accommodate this type, the Proof module also gains the map_structured_proof that takes a Proof.proof and a function on the individual goals (in the context of an evar map) and produces a structured goal based on the goal transformer. | |||
| 2014-10-01 | Add additional location information to AST XMLs. | Carst Tankink | |
| 2014-10-01 | coq_makefile: build and install *top.cmxs plugins | Enrico Tassi | |
| These plugins, like coqidetop, stmworkertop and tacworkertop are intended for toploop replacements (see -toploop command line option). With this commit coq_makefile can be used as the build system for any user-interface-specific plugins. | |||
| 2014-10-01 | Removing test for bug #2080. | Pierre-Marie Pédrot | |
| Naming a Ltac definition like a built-in tactic used to fail, but now only spits out a warning. This is too complicated to test... | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |