aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Compile OS X binaries without native_compute support.Gravatar Maxime Dénès2016-01-21
|
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| | | | | Function is_constructor was not properly fixed. Additionally, this fixes a problem with the 8.5 interpretation of in-pattern (see Cases.v).
* Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
| | | | | | | | 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.
* Fixing a minor problem in Makefile.build that was prevening ↵Gravatar Matej Kosik2015-12-07
| | | | "dev/printers.cma" to be loadable within "ocamldebug".
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
|
* Update history of revisions.Gravatar Hugo Herbelin2015-12-02
|
* MacOS package script: do not fail if link to /Applications already exists.Gravatar Maxime Dénès2015-11-18
|
* Being more precise and faithful about the origin of the file reportingGravatar Hugo Herbelin2015-11-16
| | | | about the prehistory of Coq.
* MacOS package script: do not fail if directory _dmg already exists.Gravatar Maxime Dénès2015-11-13
|
* Script building MacOS package.Gravatar Maxime Dénès2015-11-12
|
* Fixing another instance of bug #3267 in eauto, this time in theGravatar Hugo Herbelin2015-10-29
| | | | | | presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger.
* Refine Gregory Malecha's patch on VM and universe polymorphism.Gravatar Maxime Dénès2015-10-28
| | | | | | | | | | | | | | | | - 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.
* Adds support for the virtual machine to perform reduction of universe ↵Gravatar Gregory Malecha2015-10-28
| | | | | | | | 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.
* Reverting modifications in dev/top_printers pushed mistakenly.Gravatar Pierre-Marie Pédrot2015-10-14
|
* Fixing perfomance issue of auto hints induced by universes.Gravatar Pierre-Marie Pédrot2015-10-14
| | | | | | | 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.
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
|
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
| | | | | Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values.
* Minor typo in universe polymorphism doc.Gravatar Maxime Dénès2015-10-09
|
* Updating versions history with data from Gérard.Gravatar Hugo Herbelin2015-10-02
| | | | Adding Gérard's history file about V1-V5 versions.
* Update the history of versions with recent versions.Gravatar Hugo Herbelin2015-10-02
|
* Univs: More info for developers.Gravatar Matthieu Sozeau2015-10-02
|
* Fix Windows installer.Gravatar Guillaume Melquiond2015-09-17
| | | | | The theories/ directory contains no cmi/cmxs files when native_compute is disabled, so do not try to ship them.
* windows build scripts made more accurate in detecting failuresGravatar Enrico Tassi2015-08-17
|
* A printer for printing constants of the env (maybe useful when there are not ↵Gravatar Hugo Herbelin2015-07-30
| | | | too many of them).
* adding a missing case for printing zippers.Gravatar Gregory Malecha2015-07-23
|
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
| | | | | | | | | | | | | | | | | | | | | | | | 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
* win: compile with -debugGravatar Enrico Tassi2015-06-29
|
* Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
| | | | This allows fatal_error to be used for printing anomalies at loading time.
* script to build 64 coq installer for windowsGravatar Enrico Tassi2015-06-01
|
* Fixing #4198 (looking for subterms also in the return clause of match).Gravatar Hugo Herbelin2015-04-21
| | | | | This is actually not so perfect because of the lambdas in the return clause which we would not like to look in.
* use a more compact representation of non-constant constructorsGravatar Benjamin Gregoire2015-03-27
| | | | | | 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
* fix compilationGravatar Benjamin Gregoire2015-03-26
|
* Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Gravatar Pierre-Marie Pédrot2015-02-19
|
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
| | | | | | (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
| | | | | | | 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).
* Windows installer cleanupGravatar Enrico Tassi2015-02-05
|
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
|
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
| | | | printing functions touched in the kernel).
* vm_printers: fix compilationGravatar Enrico Tassi2015-01-15
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
|
* Compatibility ocaml 3.12.Gravatar Hugo Herbelin2014-12-30
|
* Minor fixes for the win32 installerGravatar Enrico Tassi2014-12-30
|
* Win32: fix installerGravatar Enrico Tassi2014-12-19
| | | | | Still unsure about .o file (should they be shipped for the native_compute machinery or .cmxs suffice?)
* More printers for ltac signatures.Gravatar Hugo Herbelin2014-12-16
|
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* Removing import of Proofview in debugger because its module Goal hidesGravatar Hugo Herbelin2014-12-07
| | | | | the import of goal.ml and, afaiu, ocaml does not provide a way to refer to a shadowed module.
* More printers in tracer.Gravatar Hugo Herbelin2014-12-05
|
* Reactivating option "Set Printing Existential Instances" for asking printing ↵Gravatar Hugo Herbelin2014-12-04
| | | | full instances.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 20:25:35 +0000