| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-17 | Dedicated file for universe unification context manipulation. | Pierre-Marie Pédrot | |
| This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar. | |||
| 2015-10-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-10 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-06 | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot | |
| 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. | |||
| 2015-10-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Univs: More info for developers. | Matthieu Sozeau | |
| 2015-09-20 | Better debug printers for module paths. | Maxime Dénès | |
| Now distinguishes between bound modules (Top#X) and submodules (Top.X). Could be useful for the regular printer as well (e.g. in error messages), but I don't know what the compatibility constraints are, so leaving it as it is for now. | |||
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 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-22 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-08-17 | windows build scripts made more accurate in detecting failures | Enrico Tassi | |
| 2015-08-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-27 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-23 | adding a missing case for printing zippers. | Gregory Malecha | |
| 2015-07-02 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 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-26 | dev/tool/anomaly-traces-parser.el | Gabriel Scherer | |
| An .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output. | |||
| 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-23 | 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-22 | Merge remote-tracking branch 'forge/v8.5' | Pierre Boutillier | |
| 2015-06-01 | script to build 64 coq installer for windows | Enrico Tassi | |
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-27 | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot | |
| together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |