| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 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. | |||
| 2014-11-27 | Reverting the following block of three commits: | Hugo Herbelin | |
| - Registering strict implicit arguments systematically (35fc7d728168) - Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6) - Fixing Coq compilation (894a3d16471) Systematically computing strict implicit arguments can lead to big computations, so I suspend this attempt, waiting for improved computation of implicit arguments, or alternative heuristics going toward having more conversion in rewrite. | |||
| 2014-11-26 | Experimenting always forcing convertibility on strict implicit arguments | Hugo Herbelin | |
| in tactic unification. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |