| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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/*/ | |||
| 2014-03-02 | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey | |
| NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml | |||
| 2014-03-02 | Removing generic equality in Syntax plugin. | Pierre-Marie Pédrot | |
| 2014-03-02 | Adding an equality function over glob_constr | Pierre-Marie Pédrot | |
| 2014-03-02 | Fixing generic Hashtbl.hash in Constr. | Pierre-Marie Pédrot | |
| 2014-03-02 | Fix syntax highlighting of "Implicit Arguments" for gtksourceview. | Guillaume Melquiond | |
| 2014-03-01 | Fixing pervasive comparisons | Pierre-Marie Pédrot | |
| 2014-03-01 | Better behaviour for sets of reserved names. | Pierre-Marie Pédrot | |
| 2014-03-01 | Never suppress the typing constraint of bound variables whose name was | Pierre-Marie Pédrot | |
| reserved with Implicit Type. | |||
| 2014-03-01 | Fixing bad comparison in Detyping. | Pierre-Marie Pédrot | |
| 2014-03-01 | Useless check when loading notations through import. | Pierre-Marie Pédrot | |
| 2014-03-01 | Hunting pervasive equality in native compiler. It seems they were used for | Pierre-Marie Pédrot | |
| optimization purposes. I replaced their use with the under-approximation of pointer equality. | |||
| 2014-03-01 | Removing a fishy use of pervasive equality in Ltac backtrace printing. | Pierre-Marie Pédrot | |
| 2014-02-28 | Removing Pervasives.compare in Termdn. | Pierre-Marie Pédrot | |
| 2014-02-28 | Removing a Pervasives.compare in Term_dnet. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |