aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* Fixing bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
|
* Do not prepend a "Error:" header when the error is expected by the user.Gravatar Guillaume Melquiond2015-03-05
| | | | | This commit also removes the extraneous "=>" token from Fail messages and prevents them from losing all the formatting information.
* Fixing OCaml 3.12 compilation.Gravatar Pierre-Marie Pédrot2015-02-27
|
* Fixing bug #3249.Gravatar Pierre-Marie Pédrot2015-02-27
| | | | | | | Instead of substituting carelessly the recursive names in Ltac interpretation, we declare them in the environment beforehand, so that they get globalized as themselves. We restore the environment afterwards by transactifying the globalization procedure.
* Univs: Fix Check calling the kernel to retype in the wrong environment.Gravatar Matthieu Sozeau2015-02-24
| | | | Fixes bug #4089.
* Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Gravatar Pierre-Marie Pédrot2015-02-19
|
* Fix bug #4046.Gravatar Matthieu Sozeau2015-02-18
|
* Remove Whelp commands.Gravatar Maxime Dénès2015-02-17
| | | | | | Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive.
* Fix bug #3960: potential evar instance categorized as an unresolvableGravatar Matthieu Sozeau2015-02-16
| | | | goal in Instance. Also remove some dead code.
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
| | | | Of course such proofs cannot be processed asynchronously
* Better error message for nested module application.Gravatar Maxime Dénès2015-02-13
| | | | Fixes #3809.
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
|
* 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.
* Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
| | | | This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
|
* 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).
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-11
| | | | | This is a fixup of commit 2e09a22b that used uniquely generated kernel names but forgot to substitute them.
* Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ↵Gravatar Hugo Herbelin2015-02-10
| | | | declarations).
* Properly set module names in presence of -Q. (Fix for bug #3958)Gravatar Guillaume Melquiond2015-02-05
| | | | | | | | This is done by adding a fourth type of loadpath, the ones that are neither implicit nor root, for the subdirectories of a -Q root. Note: this means that scanning for available directories is no longer done on the fly for -Q, but once and for all, as with -R.
* Optimized Import/Export the same way as Require Import/Export wasGravatar Hugo Herbelin2015-02-04
| | | | | | optimized. Now "Import Arith ZArith" imports only once the libraries reexported by both Arith and ZArith. (No side effect can be inserted here, so that this looks compatible).
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-04
|
* Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Gravatar Enrico Tassi2015-02-03
| | | | This reverts commit 2e09a22baeb93c57e6d8388313dc638349679910.
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-03
|
* spit module path using / as directory separatorGravatar Enrico Tassi2015-02-03
| | | | | | | | I know it seems wrong but if you call coq to get a path, you are likely to pass it around, and this makes the dir separator of windows "\" disappear immediately being interpreted as an escape character. In cygwin "/" is also understood as a directory separator.
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
|
* Prevent spurious warnings about Arguments.Gravatar Guillaume Melquiond2015-01-29
| | | | | | | | | | | | | The Arguments command tends to emit the following warning even when properly used: This command is just asserting the number and names of arguments of cons. If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes' In fact, even ': assert' does not silence it, contrarily to what the message suggests.
* Equality Schemes options: reverting commit ff9f94634 which isGravatar Hugo Herbelin2015-01-24
| | | | | | | obviously inconsistent with the decisions taken in commits 2e8fb20e04da and 0bc569026048 about bugs #2550 and #3606. Now having options Boolean Equality Schemes and Decidable Equality Schemes.
* Isolate a function for printing evar sets.Gravatar Hugo Herbelin2015-01-24
|
* Add the possibility of defining opaque terms with program.Gravatar mlasson2015-01-21
|
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
| | | | printing functions touched in the kernel).
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
| | | | | One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem.
* Make -print-mod-uid accept a list of files.Gravatar Maxime Dénès2015-01-15
| | | | Solves an efficiency problem in Makefiles generated by coq_makefile.
* Made -print-mod-uid more silent and robust.Gravatar Maxime Dénès2015-01-13
| | | | This is a follow-up on Pierre's 5d80a385.
* Add -no-native-compiler flag to list dumped by --help.Gravatar Maxime Dénès2015-01-12
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Avoiding a redundant information in unification error message.Gravatar Hugo Herbelin2015-01-11
|
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
|
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
| | | | | | Removing unused argument and fixing bug #3899, now warning when a record cannot be made primitive in Set Primitive Projections mode because it has no projection or at least one undefinable projection.
* In Show Universes, print universes before normalization.Gravatar Matthieu Sozeau2015-01-05
|
* Fixing bug #3632 for good.Gravatar Pierre-Marie Pédrot2014-12-29
|
* Proof using: do not clear letins (unless they use a cleared var)Gravatar Enrico Tassi2014-12-29
|
* Proof using: call "clear" to remove from sight the vars not selectedGravatar Enrico Tassi2014-12-28
| | | | | | | As discussed on coqdev, clear is not perfect, Hints for trivial using cleared section vars are still used. But it is better than nothing I guess.
* remove debug prints (leftover)Gravatar Enrico Tassi2014-12-28
|
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
|
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
|
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
|
* Arguments: warn only if no option is given (Close 3860)Gravatar Enrico Tassi2014-12-17
|
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 20:39:00 +0000