| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-03-03 | Replacing arguments of Trie by a cancellable monoid. | Pierre-Marie Pédrot | |
| 2014-03-03 | Fixing generic hashes and replacing them with proper ones. | Pierre-Marie Pédrot | |
| 2014-03-02 | Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) | Pierre Letouzey | |
| There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching. | |||
| 2014-03-02 | Set officially the minimal OCaml requirement to 3.12.1 | Pierre Letouzey | |
| Anyway, a few syntactic features of 3.12 were already used here and there (e.g. local opening via Foo.(...), or the record shortcut { field; ... }). Hence compiling with 3.11 wasn't working anymore. Already take advantage of the following 3.12.1 features : - "module type of ..." in CArray, CList, CString ... - "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output via our coqdep to localize the .ml4 modules :-) The -ml-synonym option (+ various bugfixes) is the reason for asking 3.12.1 directly and not just 3.12.0. After all, if debian stable is providing 3.12.1, then everybody has it ;-) | |||
| 2014-03-02 | Makefile: the initial build of grammar.cma is now directory-driven | Pierre Letouzey | |
| In last commit, we used grep to decide whether a .ml4 could be compiled during the initial phase of not. Instead, we now rely on a simpler directory dichotomy: - config lib kernel library pretyping interp parsing grammar are considered initial (and shouldn't contain grammar-dependent .ml4), see $(GRAMSRCDIRS) in Makefile.common - the grammar-dependent .ml4 could be in any other directories Currently, they are in: tactics toplevel plugins/* | |||
| 2014-03-02 | Migrate back g_obligations in toplevel | Pierre Letouzey | |
| This almost reverts commit 845d6f (r15248). It isn't ideal to put syntactic stuff in the toplevel directory. Maybe this kind of files should have someday their own directory along with g_rewrite.ml4 and some other (maybe a extraparsing dir?). Meanwhile, this commit leads to a cleaner situation concerning *.ml4: - everything needed to build grammar.cma (and q_constr.cmo) is in: lib/ kernel/ library/ pretyping/ interp/ proofs/ parsing/ grammar/ - all *.ml4 using grammar.cma (or q_constr.cmo) are in: tactics/ toplevel/ plugins/*/ | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |