| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-21 | Compile OS X binaries without native_compute support. | Maxime Dénès | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-13 | Fixing #4467 (continued). | Hugo Herbelin | |
| Function is_constructor was not properly fixed. Additionally, this fixes a problem with the 8.5 interpretation of in-pattern (see Cases.v). | |||
| 2016-01-05 | Fix order of files in mllib. | Maxime Dénès | |
| CString was linked after Serialize, although the later was using CString.equal. This had not been noticed so far because OCaml was ignoring functions marked as external in interfaces (which is the case of CString.equal) when considering link dependencies. This was changed on the OCaml side as part of the fix of PR#6956, so linking was now failing in several places. | |||
| 2015-12-07 | Fixing a minor problem in Makefile.build that was prevening ↵ | Matej Kosik | |
| "dev/printers.cma" to be loadable within "ocamldebug". | |||
| 2015-12-07 | Fix some typos. | Guillaume Melquiond | |
| 2015-12-02 | Update history of revisions. | Hugo Herbelin | |
| 2015-11-18 | MacOS package script: do not fail if link to /Applications already exists. | Maxime Dénès | |
| 2015-11-16 | Being more precise and faithful about the origin of the file reporting | Hugo Herbelin | |
| about the prehistory of Coq. | |||
| 2015-11-13 | MacOS package script: do not fail if directory _dmg already exists. | Maxime Dénès | |
| 2015-11-12 | Script building MacOS package. | Maxime Dénès | |
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin | |
| presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger. | |||
| 2015-10-28 | Refine Gregory Malecha's patch on VM and universe polymorphism. | Maxime Dénès | |
| - Universes are now represented in the VM by a structured constant containing the global levels. This constant is applied to local level variables if any. - When reading back a universe, we perform the union of these levels and return a [Vsort]. - Fixed a bug: structured constants could contain local universe variables in constructor arguments, which has to be prevented. Was showing up for instance when evaluating [cons _ list (nil _)] with a polymorphic [list] type. - Fixed a bug: polymorphic inductive types can have an empty stack. Was showing up when evaluating [bool] with a polymorphic [bool] type. - Made a few cosmetic changes. Patch written with Benjamin Grégoire. | |||
| 2015-10-28 | Adds support for the virtual machine to perform reduction of universe ↵ | Gregory Malecha | |
| polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions. | |||
| 2015-10-14 | Reverting modifications in dev/top_printers pushed mistakenly. | Pierre-Marie Pédrot | |
| 2015-10-14 | Fixing perfomance issue of auto hints induced by universes. | Pierre-Marie Pédrot | |
| Instead of brutally merging the whole evarmap coming from the clenv, we remember the context associated to the hint and we only merge that tiny part of constraints. We need to be careful for polymorphic hints though, as we have to refresh them beforehand. | |||
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-09 | Code cleaning in VM (with Benjamin). | Maxime Dénès | |
| Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values. | |||
| 2015-10-09 | Minor typo in universe polymorphism doc. | Maxime Dénès | |
| 2015-10-02 | Updating versions history with data from Gérard. | Hugo Herbelin | |
| Adding Gérard's history file about V1-V5 versions. | |||
| 2015-10-02 | Update the history of versions with recent versions. | Hugo Herbelin | |
| 2015-10-02 | Univs: More info for developers. | Matthieu Sozeau | |
| 2015-09-17 | Fix Windows installer. | Guillaume Melquiond | |
| The theories/ directory contains no cmi/cmxs files when native_compute is disabled, so do not try to ship them. | |||
| 2015-08-17 | windows build scripts made more accurate in detecting failures | Enrico Tassi | |
| 2015-07-30 | A printer for printing constants of the env (maybe useful when there are not ↵ | Hugo Herbelin | |
| too many of them). | |||
| 2015-07-23 | adding a missing case for printing zippers. | Gregory Malecha | |
| 2015-06-29 | Assumptions: more informative print for False axiom (Close: #4054) | Enrico Tassi | |
| When an axiom of an empty type is matched in order to inhabit a type, do print that type (as if each use of that axiom was a distinct foo_subproof). E.g. Lemma w : True. Proof. case demon. Qed. Lemma x y : y = 0 /\ True /\ forall w, w = y. Proof. split. case demon. split; [ exact w | case demon ]. Qed. Print Assumptions x. Prints: Axioms: demon : False used in x to prove: forall w : nat, w = y used in w to prove: True used in x to prove: y = 0 | |||
| 2015-06-29 | win: compile with -debug | Enrico Tassi | |
| 2015-06-25 | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly. | Thomas Sibut-Pinote | |
| This allows fatal_error to be used for printing anomalies at loading time. | |||
| 2015-06-01 | script to build 64 coq installer for windows | Enrico Tassi | |
| 2015-04-21 | Fixing #4198 (looking for subterms also in the return clause of match). | Hugo Herbelin | |
| This is actually not so perfect because of the lambdas in the return clause which we would not like to look in. | |||
| 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 | fix compilation | Benjamin Gregoire | |
| 2015-02-19 | Adding a possible DEPRECATED flag to VERNAC EXTEND statements. | Pierre-Marie Pédrot | |
| 2015-02-12 | Revert "Using same code for browsing physical directories in coqtop and coqdep." | Hugo Herbelin | |
| (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. | |||
| 2015-02-12 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error). | |||
| 2015-02-05 | Windows installer cleanup | Enrico Tassi | |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot | |
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | |
| printing functions touched in the kernel). | |||
| 2015-01-15 | vm_printers: fix compilation | Enrico Tassi | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2015-01-08 | Avoiding introducing yet another convention in naming files. | Hugo Herbelin | |
| 2014-12-30 | Compatibility ocaml 3.12. | Hugo Herbelin | |
| 2014-12-30 | Minor fixes for the win32 installer | Enrico Tassi | |
| 2014-12-19 | Win32: fix installer | Enrico Tassi | |
| Still unsure about .o file (should they be shipped for the native_compute machinery or .cmxs suffice?) | |||
| 2014-12-16 | More printers for ltac signatures. | Hugo Herbelin | |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | |
| 2014-12-07 | Removing import of Proofview in debugger because its module Goal hides | Hugo Herbelin | |
| the import of goal.ml and, afaiu, ocaml does not provide a way to refer to a shadowed module. | |||
| 2014-12-05 | More printers in tracer. | Hugo Herbelin | |
| 2014-12-04 | Reactivating option "Set Printing Existential Instances" for asking printing ↵ | Hugo Herbelin | |
| full instances. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |