aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* 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).
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
|
* Fixing use of arguments renaming in apply which was broken afterGravatar Hugo Herbelin2014-10-01
| | | | | reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f: using renaming also in retyping.
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
|
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
| | | | | | | | so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
* win32: embed NSIS for plugin writersGravatar Enrico Tassi2014-09-19
|
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
| | | | | | | Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit.
* win32: remove outdated splash screenGravatar Enrico Tassi2014-09-17
| | | | | The official Coq logo does not work as a splash screen. Simplest fix: no splash screen.
* win32: use subsystem windows on windows (and not console)Gravatar Enrico Tassi2014-09-17
| | | | This makes the hammer tools/mkwinapp.ml kind of obsolete
* Fix base_include due to change in argument order of env and evar_mapGravatar Matthieu Sozeau2014-09-12
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 23:31:42 +0000