| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-03-18 | Remove the -fno-defer-pop cflag | Jason Gross | |
| According to http://caml.inria.fr/mantis/view.php?id=6346, this flag causes ocamlc to fail on the latest version of xcode, because clang now errors on -fno-defer-pop. According to the same issue, -fno-defer-pop is required for computed gotos if you're using gcc 1.xx, but not gcc 3.4.0 nor 4.4.7 (nor presumably other reasonably modern versions of gcc). I haven't actually tested this, as I don't have a mac, but it's a relatively small change. Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org> | |||
| 2014-03-18 | Printing backtraces in coqchk while in debug mode. | Pierre-Marie Pédrot | |
| 2014-03-18 | Fixing checker with respect to new kernel name structure and hashmaps. | Pierre-Marie Pédrot | |
| Some wrong generic equalities and hashes were removed too. | |||
| 2014-03-18 | STM: make the slave start from the most recent known state | Enrico Tassi | |
| 2014-03-18 | STM: make -async-proofs on work from coqc too | Enrico Tassi | |
| 2014-03-17 | Evarconv: exact_ise_stack looks to stack head before bodies or branches | Pierre Boutillier | |
| the order of the inspection is a "random" choise but going back to the old behavior makes the compilation of ssreflect/rat.v 5 times faster ... | |||
| 2014-03-17 | Fix test-suite 2255.v | Pierre Boutillier | |
| 2014-03-16 | consider_remaining_unif_problems respects Conv_oracle | Pierre Boutillier | |
| 2014-03-14 | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot | |
| no particular purpose. | |||
| 2014-03-13 | nanoPG: better copy/paste | Enrico Tassi | |
| 2014-03-13 | fix compilation with ocaml < 4 | Enrico Tassi | |
| 2014-03-13 | STM: perspective (tell the scheduler what the user sees) | Enrico Tassi | |
| 2014-03-13 | Stateid: export a Set module | Enrico Tassi | |
| 2014-03-13 | STM: move out a couple of submodules | Enrico Tassi | |
| These modules are not as reusable as one may want them to be, but moving them out simplifies a little STM. | |||
| 2014-03-12 | fake_ide: fix compilation | Enrico Tassi | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |