| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-03-27 | Properly handle extra "clean" targets with coq_makefile. | Guillaume Melquiond | |
| 2015-03-27 | use a more compact representation of non-constant constructors | Benjamin Gregoire | |
| for which there corresponding tag are greater than max_variant_tag. The code is a merge with the patch proposed by Bruno on github barras/coq commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c | |||
| 2015-03-26 | allows the vm to deal with inductive type with 8388607 constant constructors ↵ | Benjamin Gregoire | |
| and 8388851 non-constant constructor. | |||
| 2015-03-26 | fix compilation | Benjamin Gregoire | |
| 2015-03-26 | Fix bug 4157, | Benjamin Gregoire | |
| change the representation of inductive constructor when there is too many non constant constructors in the inductive type Conflicts: kernel/cbytegen.ml | |||
| 2015-03-26 | add coqdep in distributed_exec, else make does not work. | Benjamin Gregoire | |
| 2015-03-26 | STM: change how proof mode switching commands are handled (decl_mode) | Enrico Tassi | |
| This is likely to make nested proofs containing proof modes switch broken, but fixes the problems Arnaud has in his branch. It is possible that the classification function we have today is not fine grained enough. If a command that changes the proof mode has as the only global effect changing the proof mode, then the current code is fine. If it has a more global effect that persists after the proof is over but has no impact on the proof itself, then the old code is fine. As far as I can get, the proof mode switching commands have a global effect (changing parser) but also a proof effect (un/focusing). We don't have a classification for these. Today a command having a global effect is played twice: on the proof branch an on master. Of course if such command cannot work on master (where there is no finished proof for example) we need a special treatment for it. | |||
| 2015-03-25 | Fix vm compiler to refuse to compile code making use of inductives with | Matthieu Sozeau | |
| more than 245 constructors (unsupported by OCaml's runtime). | |||
| 2015-03-25 | More clever representation of substituted Cemitcode. | Pierre-Marie Pédrot | |
| Module substitution is made nodewise, allowing to drop it for opaque terms in the VM. This saves a few useless substitutions. | |||
| 2015-03-25 | Summary: fix code to detect functional values in summary | Enrico Tassi | |
| 2015-03-25 | STM: avoid processing asynchronously empty proofs (Close: #4134) | Enrico Tassi | |
| 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |