| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-03-25 | Exporting memory representation of STM tasks for votour. | Pierre-Marie Pédrot | |
| 2015-03-25 | Fully fixing bug #3491 (anomaly when building _rect scheme in the | Hugo Herbelin | |
| presence of let-ins and recursively non-uniform parameters). The bug was in the List.chop of Inductiveops.get_arity which was wrong in the presence of let-ins and recursively non-uniform parameters. The bug #3491 showed up because, in addition to have let-ins, it was wrongly detected as having recursively non-uniform parameters. Also added some comments in declarations.mli. | |||
| 2015-03-25 | Another example about the consequence of a wrong computation of the | Hugo Herbelin | |
| number of recursively uniform parameters in the presence of let-ins. In practice, more recursively non-uniform parameters were assumed and this was used especially for checking positivity of nested types, leading to refusing more nested types than necessary (see Inductive.v). | |||
| 2015-03-25 | Use kernel names instead of user names when looking for coercions. (Fix for ↵ | Guillaume Melquiond | |
| bug #4133) Note that, if someone was purposely modifying the user name of a type in order to disable a coercion, it no longer works. Hopefully, no one did. | |||
| 2015-03-25 | coqc: fix --help | Enrico Tassi | |
| 2015-03-25 | Correcting a bug introduced by universes polymorphism | jforest | |
| 2015-03-25 | correcting a bug with aliased when using Functional Scheme | forest | |
| 2015-03-24 | Updating test-suite (see previous commit). | Hugo Herbelin | |
| 2015-03-24 | Fixing computation of non-recursively uniform arguments in the | Hugo Herbelin | |
| presence of let-ins. This fixes #3491. | |||
| 2015-03-24 | Fixing wrong rel_context in checking positivity condition. | Hugo Herbelin | |
| Parameters were missing in the context, apparently without negative effects because the context was used only for whd normalization of types, while reduction (in closure.ml) was resistant to unbound rels. See however next commit for an indirect effect on the wrong computation of non recursively uniform parameters producing an anomaly when computing _rect schemas. | |||
| 2015-03-24 | Functorized interface over object representation in votour. | Pierre-Marie Pédrot | |
| This gives more safety in object manipulation, as we delimit the uses of Obj functions, and allows for an alternative implementation of the representation of OCaml structures. | |||
| 2015-03-24 | Fixing representation of dynamics in votour (again). | Pierre-Marie Pédrot | |
| 2015-03-24 | Fixing equality of notation_constrs. Fixes bug #4136. | Pierre-Marie Pédrot | |
| 2015-03-24 | Revert "Useless check when loading notations through import." | Pierre-Marie Pédrot | |
| This reverts commit 124734fd2c523909802d095abb37350519856864. | |||
| 2015-03-23 | Dedicated type for on-demand objects in Library. | Pierre-Marie Pédrot | |
| 2015-03-23 | coqchk: more prints when -debug | Enrico Tassi | |
| 2015-03-23 | Load: don't give anomaly on aborted proofs (Close: #3882) | Enrico Tassi | |
| 2015-03-22 | Announcing * and ** which were not official yet in 8.4. | Hugo Herbelin | |
| 2015-03-22 | Qed export -> Qed exporting | Enrico Tassi | |
| 2015-03-22 | Aliasing give_up with admit | Enrico Tassi | |
| 2015-03-22 | STM: if Set Universe Polymorphism then synchronous (#4119) | Enrico Tassi | |
| It was detecting only the per-lemma Polymorphic flag, but not the global one. | |||
| 2015-03-22 | STM: do not delegate proofs containing Print | Enrico Tassi | |
| 2015-03-22 | STM: after every command restore the expected proof mode | Enrico Tassi | |
| 2015-03-22 | typo | Enrico Tassi | |
| 2015-03-21 | Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107) | Guillaume Melquiond | |
| 2015-03-21 | Avoid segfault from code extracted to ghc. (Fix for bug #1257) | Guillaume Melquiond | |
| 2015-03-21 | Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221) | Guillaume Melquiond | |
| 2015-03-21 | Do not revert parameter lists when extracting singleton types to Haskell. ↵ | Guillaume Melquiond | |
| (Fix for bugs #3470 and #3694) | |||
| 2015-03-20 | Fixed #4138. In emacs mode Set/Unset does not print the goal anymore. | Pierre Courtieu | |
| In PG there are shortcuts that perform on the fly "Set Printing All"/"Unset Printing All" in pg. For example if you type C-u before some shortcut for print (check/About/Show), it performs: Set Printing All. Print foo. Unset Printing All. But if the "Unset" prints a goal, then pg interprets the output of Print as a command applied on a previous line, and thus hides it. So for emacs mode I would prefer no goal printing when options are set/unset. In the situation where this should be done (when setting durably the option probably), I'd rather program a "Show" explicitely. | |||
| 2015-03-18 | More sharing in module substitution. | Pierre-Marie Pédrot | |
| 2015-03-18 | add -type-in-type to the usage message | Daniel R. Grayson | |
| 2015-03-18 | Fixing internal representation of Dyn.t in votour. | Pierre-Marie Pédrot | |
| 2015-03-17 | Add function to fix the non-substituted universe variables of an evar_map. | Matthieu Sozeau | |
| 2015-03-16 | Removing the whole library content from the summary. | Pierre-Marie Pédrot | |
| It is still present in the libstack, though. | |||
| 2015-03-16 | More invariants in Library. | Pierre-Marie Pédrot | |
| We explicit the fact that we only need the name of the library in most of the summaries. | |||
| 2015-03-16 | gitattributes: add `.mailmap` file to the list of files excluded from the ↵ | Arnaud Spiwack | |
| `.tar.gz`. | |||
| 2015-03-16 | Gitattributes file added to generate archive. | Guillaume Claret | |
| Cherry-picked from v8.4 ( c1aabb104122ead02fa289339a42815373338222 ). | |||
| 2015-03-16 | Adding a primitive to dump the current association table of dynamic types. | Pierre-Marie Pédrot | |
| 2015-03-15 | STM: -debug: better explanation of why not async (#4125) | Enrico Tassi | |
| 2015-03-15 | STM: -quick: async no Proof using but no Section (#4124) | Enrico Tassi | |
| As happens in interactive mode. | |||
| 2015-03-14 | End of Bug 3986 - make cleanall removes .*.aux files | Pierre Boutillier | |
| 2015-03-14 | Bug 3981 ends to convice me that subdirs in coq_makefile deverse a warning | Pierre Boutillier | |
| 2015-03-14 | Fix Bug 3548 - Makefile should fallback gracefully in the absence of codesign | Pierre Boutillier | |
| 2015-03-13 | Fix compilation with forthcoming Ocaml version 4.03. | Arnaud Spiwack | |
| Backported from a patch for v8.4 by Pierre Chambart. Part of the commit has been rendered obsolete by code reorganisation, leaving: * OCaml runtime header files used to declare the int32, uint32, int64 and uint64 type. That got removed, and uses of those types should be replaced by the standard ones: uint32_t, int32_t, int64_t, uint64_t. Those are defined in stdint.h. | |||
| 2015-03-13 | Declarative mode: make it so that unfocussing can only be done for closed ↵ | Arnaud Spiwack | |
| subproofs. The front-end is supposed to take care of that, but it may help to catch bugs. | |||
| 2015-03-13 | Declarative mode: remove dead code. | Arnaud Spiwack | |
| 2015-03-13 | Declarative mode: remove a superfluous [set_proof_mode]. | Arnaud Spiwack | |
| It was probably creating bugs when trying to use [escape]. | |||
| 2015-03-13 | Declarative mode: fix the focus behaviour. | Arnaud Spiwack | |
| I had previously mistakenly enforced the property that after solving every goal in a block, unfocusing was performed automatically until one goal is in focus. This is not how the declarative mode is supposed to behave. Rather every focus must be explicitely unfocused by a closing command. This hit a few bad interaction with the pure representation of proof introduced for the asynchronous processing. Some of the invariants seem fragile, so this minimally disruptive solution is probably not long-term. In particular since each block uses the same focus kind, an `end <block>` may close another block than intended if the number of unfocussing command executed is not the right one. | |||
| 2015-03-13 | rewiring Czar printers that were disabled | Pierre Corbineau | |
| Backported from trunk. | |||
| 2015-03-13 | CHANGES: more correct equivalent to "constructor tac" syntax. | Arnaud Spiwack | |
| As mentionne in #3969, using "once (constructor;tac)" leads in exponential blowups, whereas "[> once (constructor;tac) ..]" does not. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |