aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* Fix a bug of Mltop.declare_cache_object.Gravatar Pierre-Marie Pédrot2016-10-05
| | | | | | | Objects registered through the callback functions were pushed on the libstack before the ML-MODULE object itself, leading to anomalies when the corresponding object was assuming that the ML module was properly defined in any other Coq module requiring the Declare ML command.
* Changing the separator for appended string options to comma.Gravatar Maxime Dénès2016-10-04
| | | | | | This is a bit ad-hoc, but looks better for warnings since there is a command-line flag accepting the same values, so comma will lead to fewer parsing issues than space.
* Allow appending to string options.Gravatar Guillaume Melquiond2016-10-01
| | | | | | | Whether an option should be set or appended to is stored as a 2-value flag next to the new content. This commit also cleans the code by declaring a single object for each persistent option rather than three different ones (one per locality).
* Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
|\ | | | | | | | | Was PR#299: Fix bug #4869, allow Prop, Set, and level names in constraints.
* | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-09-29
| | | | | | | | | | | | Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
| * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
|/
* Fix bug #5090: Effect of -Q depends on coqtop's current directory.Gravatar Pierre-Marie Pédrot2016-09-25
| | | | | | | This bug was seemingly introduced on purpose by commit 9c5ea63 in 2001. It seems that the original motivation was to deactivate a warning when overriding the default loadpath binding of the current directory, but in the end it made it non-overridable.
* Remove dead code in library/lib.ml.Gravatar Maxime Dénès2016-09-20
|
* A proposal to unify the messages given by Test and Print Options (#5062).Gravatar Hugo Herbelin2016-09-06
|
* Summary: simpler API for process-local storageGravatar Enrico Tassi2016-09-05
|
* Emit a warning on Require inside a module.Gravatar Maxime Dénès2016-08-30
|
* Send Dependency feedback only if file not already loaded.Gravatar Maxime Dénès2016-08-29
|
* Fix bug #4750: Change format of inconsistent assumptions message.Gravatar Pierre-Marie Pédrot2016-08-28
| | | | | We now print the file responsible for the incompatibility in require error messages.
* More standard naming for the Imparg.with_implicits function.Gravatar Pierre-Marie Pédrot2016-08-20
|
* Removing dead code in Impargs.Gravatar Pierre-Marie Pédrot2016-08-19
|
* COMMENT: moving misplaced comment where it belongsGravatar Matej Kosik2016-07-29
|
* 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.
* Exporting section_segment_of_reference.Gravatar Hugo Herbelin2016-06-29
|
* universes.ml: Minor code cleanupGravatar Matthieu Sozeau2016-06-29
|
* 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
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
* | Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Adding a local type-in-type flag in kernel declarations.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
| | | | | | | | | | This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase.
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
| | | | | | | | | | | | | | | | | | | | | The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
* | | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ | | | | | | | | | | | | Add -o option to coqc
* \ \ \ Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\ \ \ \
* | | | | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
| | | | * Univs: fix for part #2 of bug #4816.Gravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | Check that the polymorphic status of everything that is parameterized in nested sections is coherent.
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \ \ \ \ | | |_|_|/ | |/| | |
| | * | | LtacProf for Coq trunkGravatar Jason Gross2016-06-05
| |/ / / |/| | | | | | | | | | | | | | | | | | | This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk.
| * | | Fix incorrect checking of library checksums.Gravatar Maxime Dénès2016-06-05
| | | | | | | | | | | | | | | | | | | | | | | | Since d09def34, only the summary of libraries was included in the checksum, not the actual content of the library. This quick fix performs the checking of the checksum immediately, even if the loading is delayed.
* | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
| | * | coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The -o option lets one put .vo or .vio files in a directory of choice, i.e. decouple the location of the sources and the compiled files. This ease the integration of Coq in already existing IDEs that handle the build process automatically (eg Eclipse) and also enables one to compile/run at the same time 2 versions of Coq on the same sources. Example: b.v depending on a.v coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
* | | Dyn: simplify API introducing an Easy submoduleGravatar Enrico Tassi2016-05-13
| | | | | | | | | | | | Now the casual Dyn user does not need to be a GADT guru
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\| |
| * | Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.Gravatar Pierre-Marie Pédrot2016-05-08
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Fix bug #4292: Unexpected functor objects.Gravatar Pierre-Marie Pédrot2016-05-03
| | |
* | | Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into ↵Gravatar Matthieu Sozeau2016-04-04
|\ \ \ | | | | | | | | | | | | | | | | | | | | aspiwack-linear-comparison Fixing a -1 -> +1 typo
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ \ | | |/ / | |/| |
| * | | Fix #4607: do not read native code files if native compiler was disabled.Gravatar Maxime Dénès2016-03-04
| | | |
* | | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \ \
* \ \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ \ \ | | |/ / / | |/| | |
| | * | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published.
| * | | Optimizing the universes_of_constr_function.Gravatar Pierre-Marie Pédrot2016-02-03
| | | | | | | | | | | | | | | | | | | | Instead of relying on a costly set union, we take advantage of the fact that instances are small compared to the set of universes.
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-20 02:36:47 +0000