| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-03-12 | Stm: smarter delegation policy | Enrico Tassi | |
| Stm used to delegate every proof when it was possible, but this may be a bad idea. Small proofs may take less time than the overhead delegation implies (marshalling, etc...). Now it delegates only proofs that take >= 1 second. By default a proof takes 1 second (that may be wrong). If the file was compiled before, it reuses the data stored in the .aux file and assumes the timings are still valid. After a proof is checked, Coq knows how long it takes for real, so it wont predict it wrong again (when the user goes up and down in the file for example). CoqIDE now sends to Coq, as part of the init message, the file name so that Coq can load the .aux file. | |||
| 2014-03-12 | CoqIDE: Errors page gets red if not empty | Enrico Tassi | |
| 2014-03-12 | CoqIDE: detachable message/error/jobs panes | Enrico Tassi | |
| 2014-03-11 | vi2vo: universes handling finally fixed | Enrico Tassi | |
| Universes that are computed in the vi2vo step are not part of the outermost module stocked in the vo file. They are part of the Library.seg_univ segment and are hence added to the safe env when the vo file is loaded. The seg_univ has been augmented. It is now: - an array of universe constraints, one for each constant whose opaque body was computed in the vi2vo phase. This is useful only to print the constants (and its associated constraints). - a union of all the constraints that come from proofs generated in the vi2vo phase. This is morally the missing bits in the toplevel module body stocked in the vo file, and is there to ease the loading of a .vo file (obtained from a .vi file). - a boolean, false if the file is incomplete (.vi) and true if it is complete (.vo obtained via vi2vo). | |||
| 2014-03-11 | Fix (3243): univ constraints of module subtyping were not propagated | Enrico Tassi | |
| Universe constraints coming from subtyping were not propagated to the outermost module and hence not stocked in the .vo file. Still, they were added to the interactive safe environment and hence checked for satisfiability. | |||
| 2014-03-10 | Useless Array.to_list in Typeops. | Pierre-Marie Pédrot | |
| 2014-03-10 | Evarconv unification respects Conv_oracle | Pierre Boutillier | |
| 2014-03-10 | MaybeFlexible semantic changes | Pierre Boutillier | |
| From Maybe reducible to Maybe to reduce (but for sure reducible) | |||
| 2014-03-10 | Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r. | Guillaume Melquiond | |
| 2014-03-08 | Using HMaps in global references. | Pierre-Marie Pédrot | |
| 2014-03-08 | Also use HMaps in KNmap. | Pierre-Marie Pédrot | |
| 2014-03-07 | Potentially unused computation in Goal. | Pierre-Marie Pédrot | |
| 2014-03-07 | Useless tactic bindings in Tacticals. | Pierre-Marie Pédrot | |
| 2014-03-07 | Using Hashmaps by default in constant and inductive maps. This changes fold and | Pierre-Marie Pédrot | |
| iter order, but it seems nobody was relying on it (contrarily to the string case). | |||
| 2014-03-07 | Tentative fix for a very strange pervasive equality in Auto. | Pierre-Marie Pédrot | |
| 2014-03-07 | Compiling coqc in "tools" target. | Pierre-Marie Pédrot | |
| 2014-03-07 | Fix lookup of native files when option -R is missing. | Guillaume Melquiond | |
| Testcase: mkdir a echo "Definition t := O." > a/a.v coqc -R a a a/a.v echo "Require Import a.a. Definition u := t." > b.v coqc -I . b.v rm -rf a b.* | |||
| 2014-03-07 | Fixing generic equality in Auto. | Pierre-Marie Pédrot | |
| 2014-03-06 | Inductive maps in Environ now use HMap. | Pierre-Marie Pédrot | |
| 2014-03-06 | make install-coqlight installs DLLCOQRUN and LIBCOQRUN | Pierre Boutillier | |
| 2014-03-06 | Lets coqtop use a slash | Virgile Prevosto | |
| 2014-03-06 | Uses slashes for install and config directories | Virgile Prevosto | |
| 2014-03-06 | remove trailing '\r' from file names returned by coqtop | Virgile Prevosto | |
| 2014-03-05 | Fix typo in comment. | Maxime Dénès | |
| 2014-03-06 | Fixing interpretation of tactics in terms. It was forgetting part of the | Pierre-Marie Pédrot | |
| environment. | |||
| 2014-03-05 | Using HMaps in Safe_env.environments, hopefully improving performances. | Pierre-Marie Pédrot | |
| 2014-03-05 | Canary testing absence of generic equality for KerNames | Pierre-Marie Pédrot | |
| 2014-03-05 | Lazily computed hash in KerName.t. | Pierre-Marie Pédrot | |
| 2014-03-05 | Adding a canary library. This canary is imperfect. It allows serialization | Pierre-Marie Pédrot | |
| (hopefully), and forbids generic equality. Still, it allows generic hash. | |||
| 2014-03-05 | Fixing compilation on OCaml 4.01. | Pierre-Marie Pédrot | |
| 2014-03-05 | Fixing previous commit. Forgot to include some code. | Pierre-Marie Pédrot | |
| 2014-03-05 | Added a new module HMap. It works (almost) like Map, except that it expects | Pierre-Marie Pédrot | |
| the provided type to come with a hashing function. The internal representation is changed, such that values are first compared w.r.t. to their hash. This effectively saves a lot of comparisons which may be far more expensive than O(1), as in the string case, hence resulting in an overall speedup. CAVEAT: everything is not implemented yet, and order-sensitive functions now do not respect the provided order anymore. | |||
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey | |
| The removed code isn't used locally and isn't exported in the signature | |||
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | |
| With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment. | |||
| 2014-03-05 | Correct handling of hashconsing of constraint sets. The previous implementation | Pierre-Marie Pédrot | |
| did not respect the requirement that equality should preserve hash. | |||
| 2014-03-05 | Adding a CSet module in Coq lib. | Pierre-Marie Pédrot | |
| 2014-03-04 | Fixing pervasives equalities in Vconv. | Pierre-Marie Pédrot | |
| 2014-03-04 | Move error and job display to the lower right pane. | Guillaume Melquiond | |
| 2014-03-04 | STM: fix Show Script | Enrico Tassi | |
| 2014-03-04 | STM: when finish a task hcons universe constraints | Enrico Tassi | |
| 2014-03-03 | Fixing some generic equalities in Micromega. | Pierre-Marie Pédrot | |
| 2014-03-03 | Fixing Pervasives.equality in extraction. | Pierre-Marie Pédrot | |
| 2014-03-03 | Fixing pervasive equalities. In particular, I removed the code that deleted | Pierre-Marie Pédrot | |
| duplicates in kernel side effects. They were chosen according to an equality that was quite irrelevant, and as expected this patch did not break the test-suite. | |||
| 2014-03-03 | Removing generic hashes in kernel. | Pierre-Marie Pédrot | |
| 2014-03-03 | Getting rid of generic hashes in cc plugin. | Pierre-Marie Pédrot | |
| 2014-03-03 | Kernel names are implemented using records. | Pierre-Marie Pédrot | |
| 2014-03-03 | Goptions do not rely anymore on generic equality. | Pierre-Marie Pédrot | |
| 2014-03-03 | Term dnets do no need to contain the afferent constr pattern in their nodes. | Pierre-Marie Pédrot | |
| 2014-03-03 | Removing Termdn, and putting the relevant code in Btermdn. The current Termdn | Pierre-Marie Pédrot | |
| file was useless and duplicated code from Btermdn itself. | |||
| 2014-03-03 | Extruding code not depending of the functor argument in Termdn. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |