| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-10 | Fix segfault in native compiler on int31 division. | Maxime Dénès | |
| Thanks to Yves for reporting it! | |||
| 2014-10-09 | No need anymore for referring to xml directory in MLINCLUDES. | Hugo Herbelin | |
| 2014-10-09 | Restoring plugins/xml/README erased by mistake. | Hugo Herbelin | |
| 2014-10-09 | Propagating name of goal to main subgoal in cut and conversion tactics. | Hugo Herbelin | |
| 2014-10-09 | Added support for having one subgoal inheriting the name of its father in ↵ | Hugo Herbelin | |
| Refine. | |||
| 2014-10-09 | Removing Convert_concl and Convert_hyp from Logic. | Hugo Herbelin | |
| 2014-10-09 | A version of convert_concl and convert_hyp in new proof engine. | Hugo Herbelin | |
| Not very optimized though (if we apply convert_hyp on any hyp, a new evar will be generated for every different hyp...). | |||
| 2014-10-09 | Adding printer for named_context_val and Goal.goal in debugger. | Hugo Herbelin | |
| 2014-10-09 | Fixup leading ./ path cleaning | Pierre Boutillier | |
| 2014-10-09 | Coq_makefile: Allow empty logical names | Pierre Boutillier | |
| I'm not sure that coqdep and coqtop understand them correctly anyway ... | |||
| 2014-10-08 | fix make mlidoc | Pierre Boutillier | |
| 2014-10-08 | Fixing the anomaly in bug #3045 (a filter was not type-safe in | Hugo Herbelin | |
| 2nd-order matching). We made the filter type-safe (i.e. to ensure that Gamma |- ?n:T is well-typed when taking the filtered context Gamma) in 2nd order matching. Maybe this weakens the power of the 2nd order matching algorithm, so it is not clear that it is the good fix. Another fix could have been to ensure that taking the closure of filter does not extend it beyond the original filter (hence keeping the filter untyped if it was already untyped). As for the bug #3045, it also revealed that some "destruct c as [[]]" could be made stronger as decomposing the destruct in two parts "destruct c as [x]; destruct x" workis while it currently fails if in one part. | |||
| 2014-10-08 | Applying Virgile Prevosto's patch for better error report in coqdep (#3029). | Hugo Herbelin | |
| 2014-10-08 | Forgotten hints.ml{,i} files in 38b34dfffcc. | Hugo Herbelin | |
| 2014-10-07 | Adding a printer for hints. | Hugo Herbelin | |
| 2014-10-07 | Splitting out of auto.ml a file hints.ml dedicated to hints so as to | Hugo Herbelin | |
| being able to export hints without tactics, vm, etc. to come with. Some functions moved to the new proof engine. | |||
| 2014-10-07 | Add test-suite file for the projection unfolding bug I just fixed. | Matthieu Sozeau | |
| 2014-10-07 | Fix test-suite file 3352 which was containing the wrong test. | Matthieu Sozeau | |
| 2014-10-07 | Fix test-suite file to test original bug, not the failure of the guard | Matthieu Sozeau | |
| condition. | |||
| 2014-10-07 | Build unfolded versions of the primitive projection in let (a, p) := ... | Matthieu Sozeau | |
| to maintain compatibility (HoTT bug #557). | |||
| 2014-10-07 | Fixing #3687 (inconsistent lexer state after a bullet). | Hugo Herbelin | |
| I forgot to tell that we are again at the beginning of a line after a bullet. | |||
| 2014-10-07 | Removing debugging information committed by mistake. | Hugo Herbelin | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |