aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* -profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)Gravatar Enrico Tassi2016-09-29
| | | | | With this command line flag one can profile ltac in files /and/ trim the results without actually touching the files.
* The coqtop options -Q and -R do not affect the ML loadpath anymore.Gravatar Pierre-Marie Pédrot2016-09-25
| | | | | | It seems that such options were adding the considered path to the ML loadpath as well, which is not what is documented, and does not provide an atomic way to manipulate Coq loadpaths.
* coqc -o now places .glob file near .vo fileGravatar Enrico Tassi2016-09-22
| | | | | All compilation (by)products are placed where -o specifies. Used to be the case for .vo, .vio, .aux but not .glob
* Fix warning when using Variables at toplevel.Gravatar Maxime Dénès2016-09-19
|
* coqc: print debug feedback coming from workersGravatar Enrico Tassi2016-09-13
| | | | This way par:eauto and all:eato print the same debugging traecs
* Avoid putting a useless "toploop" directory in the ML search path if it does ↵Gravatar Guillaume Melquiond2016-09-10
| | | | not exist.
* Make it explicit when paths are added to the ML search paths.Gravatar Guillaume Melquiond2016-09-09
| | | | | | | | | | | | | | | When Mltop.add_rec_path was called to add paths to the loadpath, it was also adding the top directory to the mlpath. In particular, "theories" was added to the mlpath although it was explicitly marked "~with_ml:false". The "plugins" and "user-contribs" subdirectories were scanned twice, once for filling the loadpath and then for filling the mlpath. This patch adds an argument to Mltop.add_rec_path to explicitly control which paths from the loadpath are added to the mlpath (none, the top one, all of them). The "top" option was the single old behavior; the "none" option is used for "theories"; the "all" option is used to avoid duplicate scanning for "plugins" and "user-contribs".
* Avoid canonizing the same paths over and over.Gravatar Guillaume Melquiond2016-09-08
| | | | | | | | | | The number of path canonizations was quadratic in the number of potential plugin directories. This patch makes it linear; on a standard Coq tree, this brings the number of chdir and getcwd system calls from more than 1,000 down to about 200 at startup. This also fixes a bug where the Cd vernacular command could cause plugins to break since relative paths were used to locate them.
* Fix #4941 - ~/.coqrc file confusing locationsGravatar Maxime Dénès2016-08-30
|
* Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
|
* Do not export an internal function in Namegen.Gravatar Pierre-Marie Pédrot2016-08-25
|
* Properly compute types for assumed section variables (bug #5035).Gravatar Guillaume Melquiond2016-08-24
| | | | | | | | | | This bug was introduced by commit 34ef02fac1110673ae74c41c185c228ff7876de2 Author: Matej Kosik <m4tej.kosik@gmail.com> Date: Fri Jan 29 10:13:12 2016 +0100 CLEANUP: Context.{Rel,Named}.Declaration.t
* Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Gravatar Pierre-Marie Pédrot2016-08-24
|\
* \ Merge PR #258: "Fix newline issues" into v8.6Gravatar Pierre-Marie Pédrot2016-08-24
|\ \
* | | Arguments: give / after last ! error detection fixedGravatar Enrico Tassi2016-08-23
| | |
* | | fix get_host_port error message (#4724)Gravatar Enrico Tassi2016-08-23
| | |
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\ \ \
| * | | Fixing an anomaly in printing a unification error message.Gravatar Hugo Herbelin2016-08-20
| | | |
| | | * [pp] Fix bug 4842 (Time prints in multiple lines)Gravatar Emilio Jesus Gallego Arias2016-08-19
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit proposes a fix for https://coq.inria.fr/bugs/show_bug.cgi?id=4842 The previous feature is a bit complicated to do correctly due to the separation over who has control of the console. Indeed, `-timed` is a command line option of the batch compiler, so we resort to a hack and assume control over the console. I am not very happy with this solution but should do the job. Note that the timing event is still being sent by the standard msg mechanism. A particular point of interest is the duplication of paths between the stm and vernac.
| | * [pp] Fix newline issues.Gravatar Emilio Jesus Gallego Arias2016-08-19
| |/ |/| | | | | | | | | | | | | | | This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where we got a few cases wrong wrt to newline endings. Thanks to @herbelin for pointing it out. This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\|
| * Do not assume the "TERM" environment variable is always set (bug #5007).Gravatar Guillaume Melquiond2016-08-11
| |
* | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
|\|
| * Fix bug #3886, generation of obligations of fixesGravatar Matthieu Sozeau2016-07-29
| | | | | | | | This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\|
| * Prevent "Load" from displaying all the intermediate subgoals.Gravatar Guillaume Melquiond2016-07-07
| | | | | | | | Note that even "Load Verbose" is not supposed to display them.
| * Do not display goals in -compile-verbose mode (bug #4841).Gravatar Guillaume Melquiond2016-07-07
| | | | | | | | | | | | | | | | | | | | The -verbose family of options is only meant to echo sentences as they are processed. The patch below broke this, while fixing another issue. That other issue will be fixed in the next commit. Revert "Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its" This reverts commit 2a28c677c3c205ff453b7b5903e4c22f4de2649b.
* | Program: fix #4873: transparency option not usedGravatar Matthieu Sozeau2016-07-07
| |
* | Renaming to more generic has_dependent_elim testGravatar Matthieu Sozeau2016-07-06
| |
* | Move is_prim... to Inductiveops and correct SchemeGravatar Matthieu Sozeau2016-07-06
| | | | | | | | | | | | | | | | Now scheme will not try to build ill-typed dependent analyses on recursive records with primitive projections but report a proper error. Minor change of the API (adding one error case to recursion_scheme_error).
* | primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
| | | | | | | | | | | | | | | | When defining a (co)recursive inductive with primitive projections on, which lacks eta-conversion and hence dependent elimination, build only the associated non-dependent elimination principles, and warn about this. Also make the printing of the status of an inductive w.r.t. projections and eta conversion explicit in Print and About.
* | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
| | | | | | | | We also add a Coq86.v compat file.
* | rename toplevel/cerror.ml into explainErr.ml (too close to the new ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | lib/cErrors.ml)
* | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
| | | | | | | | For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
* | Univs: Fix bug #4726Gravatar Matthieu Sozeau2016-06-29
| | | | | | | | | | When using Record and an explicit sort constraint, the universe was wrongly made flexible and minimized.
* | Univs: earlier errors for strict univ decls #4527Gravatar Matthieu Sozeau2016-06-29
| | | | | | | | | | | | | | | | When declaring the universes of a lemma explicitely, throw an error if after minimization the type of a lemma still refers to unbound universes. This is a fix and an incompatibility, but scripts will be backwards compatible themselves. Fix another minor bug in treating universe binders for (Co)Fixpoint.
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* | Properly handle the only printing flag in Reserved Notations.Gravatar Pierre-Marie Pédrot2016-06-28
| |
* | Properly handling the only printing flag when parsing rules already exist.Gravatar Pierre-Marie Pédrot2016-06-28
| |
* | Program: refine shrinking of obligationsGravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | | | | | | | | | | | Ensure correspondence between the term and type to shrink, so that Lets are preserved when they are used relevantly in either of them. This avoids e.g. "simpl" in the shrinked hypotheses to reduce shrinking, while maintaining unsimplified types in the type of the shrinked obligations (for compatibility). Simplify Lambda, Prod case of shrinking, By invariant (we start with a term and its type), the abstraction's types correspond.
* | Rework treatment of default transparency of obligationsGravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | By default obligations defined by tactics are defined transparently or opaque according to the Obligations Transparent flag, except proofs of subset obligations which are treated as opaque by default. When the user proves the obligation using Qed or Defined, this information takes precedence, and only when the obligation cannot be Qed'ed because it contains references to a recursive function an error is raised (this prevents the guardness checker error). Shrinked obligations were not doings this correctly. Forcing transparency due to fixpoint prototypes takes precedence over the user preference. Program: do not force opacity of subset proofs, maintaining compatibility.
* | Shrink Proofs/Obligations by default and deprecateGravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | | | | | | | Fix bug in Shrink obligations with Program in the process. Fix implementation of shrink for abstract proofs - Update doc in term.mli to reflect the fact that let-in's are part of what is returned by [decompose_lam_assum].
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
* | Merge remote-tracking branch 'github/pr/223' into feedback-locationsGravatar Maxime Dénès2016-06-27
|\ \ | | | | | | | | | Was PR#223: Allow feedback messages to carry a location.
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | | | | | | | | | Cf CHANGES for details.
| * | [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
|/ / | | | | | | | | | | | | | | This is a first step to relay location info in an uniform way, as needed by warnings and other mechanisms. The location info remains unused for now, but coqtop printing could take advantage of it if so wished.
* | Merge remote-tracking branch 'github/pr/212' into trunkGravatar Maxime Dénès2016-06-20
|\ \
| * | Add file name, line number and beginning of line position to locations.Gravatar Maxime Dénès2016-06-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Coq locations already had support for this, but were containing dummy information. We now don't need anymore to reconstruct this information by browsing the file when printing an error message or enriching exceptions on the fly. It also became easier to interface with Coq since locations emitted by the lexer now always contain full information. On the API side, Loc.represent disappeared and Loc.t is now exposed as record. It is less error-prone than manipulating a tuple of 5 integers. Also, Loc.create takes 5 arguments instead of 3 and a pair.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 08:23:35 +0000