| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-13 | STM: simplify how the term part of a side effect is retrieved | Enrico Tassi | |
| Now the seff contains it directly, no need to force the future or to hope that it is a Direct opaque proof. | |||
| 2014-10-13 | library/opaqueTables: enable their use in interactive mode | Enrico Tassi | |
| Before this patch opaque tables were only growing, making them unusable in interactive mode (leak on Undo). With this patch the opaque tables are functional and part of the env. I.e. a constant_body can point to the proof term in 2 ways: 1) directly (before the constant is discharged) 2) indirectly, via an int, that is mapped by the opaque table to the proof term. This is now consistent in batch/interactive mode This is step 0 to make an interactive coqtop able to dump a .vo/.vi | |||
| 2014-10-13 | Coqinit: look in toploop/ even if configured with -local | Enrico Tassi | |
| 2014-10-13 | Mentioning incompatibility shown in #3718 and coming from #3050 | Hugo Herbelin | |
| (interpreting "match goal"'s hypotheses in scope %type). | |||
| 2014-10-12 | Tentative fix for a badly used Option.get in Reductionops. | Pierre-Marie Pédrot | |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau | |
| for the record binder of classes. This name is no longer generated in the kernel but part of the declaration. Also cleanup the interface to recognize primitive records based on an option type instead of a dynamic check of the length of an array. | |||
| 2014-10-10 | Do not expand primitive projections eagerly in evarconv, but only | Matthieu Sozeau | |
| in cases of unification with existentials requiring it. | |||
| 2014-10-10 | Give the same argument name for the record binder of type class | Matthieu Sozeau | |
| projections and regular records. Easily fixable backwards incompatibility. | |||
| 2014-10-10 | Add debug printers for projections, fix printing of evar constraints | Matthieu Sozeau | |
| and unsatisfiable constraints which were not done in the right environment. | |||
| 2014-10-10 | Add a "Debug Tactic Unification" option and correct the first-order | Matthieu Sozeau | |
| application case to expand primitive projections at the head of both applications. | |||
| 2014-10-10 | Make constrMatching and detyping more robust with respect to | Matthieu Sozeau | |
| expand_projection failing if an innapropriate sigma is given. | |||
| 2014-10-10 | Fix bug due to shadowing a variable name in tacred | Matthieu Sozeau | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |