| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-13 | Moving function about locs in locusops. | Hugo Herbelin | |
| 2014-10-13 | English typo in a function name of evarconv. | Hugo Herbelin | |
| 2014-10-13 | Added support for several impossible cases in compilation of "match". | Hugo Herbelin | |
| 2014-10-13 | Stm: more precise representation of nested proofs | Enrico Tassi | |
| This fixes the bug reported by Hugo: 2) Goal True. 3-4) Definition a:=0. 5) Goal True True. (* jumped back to 3 (on master) instead of 4 (on the outermost proof) *) | |||
| 2014-10-13 | When loading libraries, feed back dependencies. | Carst Tankink | |
| These dependencies between files can be used by UIs to guide compilation and reloading of files. FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar. FileDependency (None, "/bar.v") means the current file depends on bar. | |||
| 2014-10-13 | Emit a warning for void Arguments statement (Close 3713) | Enrico Tassi | |
| 2014-10-13 | Parsing of "?[" as two tokens (makes ssr compile). | Enrico Tassi | |
| The problem is that "?[" makes the lexer glue "?" and "[" into a single token but in ssr "?" (iteration) and "[" (rewrite pattern delimiter) are often close, but they are parsed by very hard to refactor grammar entries. To consider: - check the adjacency of the two symbols looking at the loc to parse exactly the same sentences as before this patch - change syntax completely, e.g. "(_ as id)" | |||
| 2014-10-13 | STM: primitives to snapshot a .vi while in interactive mode | Enrico Tassi | |
| 2014-10-13 | selective join/export of the safe_environment | Enrico Tassi | |
| This generalizes the BuildVi flag and lets one choose which opaque proofs are done and which not. | |||
| 2014-10-13 | TQueue: new primitive to take a snapshot of the queue | Enrico Tassi | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |