aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* 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.
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
| | | | | | | | | | | - 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.
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
| | | | in tactic unification.
* Add printer for transparent state for ocamldebug.Gravatar Hugo Herbelin2014-11-23
|
* Specific printer of Evar.Set.t for ocamldebug + more information inGravatar Hugo Herbelin2014-11-22
| | | | a UserError to ease debugging.
* Adding a pretty-printing style library.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
|
* More "open" by default for trace debugging.Gravatar Hugo Herbelin2014-10-31
|
* Split [Proofview] into a file where the basic operations on the state are ↵Gravatar Arnaud Spiwack2014-10-22
| | | | | | defined and the file providing the primitives. The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring.
* Fix ill-typed debugging functionGravatar Matthieu Sozeau2014-10-15
|
* Adding printers for ppproofview.Gravatar Hugo Herbelin2014-10-13
|
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
| | | | and unsatisfiable constraints which were not done in the right environment.
* Adding printer for named_context_val and Goal.goal in debugger.Gravatar Hugo Herbelin2014-10-09
|
* Adding a printer for hints.Gravatar Hugo Herbelin2014-10-07
|
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
| | | | | it became possible to have binding names themselves bound to ltac variables (2fcc458af16b).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 16:10:26 +0000