aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-03-22Merge PR#478: Small optimization on handling of library state.Maxime Dénès
2017-03-22Merge PR#482: [toplevel] Remove unusable option -notopMaxime Dénès
2017-03-21Merge PR#134: Enable `-safe-string`Maxime Dénès
2017-03-21trivial: fix commentMatej Kosik
2017-03-20[misc] Remove warnings about String.setEmilio Jesus Gallego Arias
The `a.[i] <- x` notation is deprecated and we were getting a couple of warnings.
2017-03-20Merge PR#479: [future] Remove unused parameter greedy.Maxime Dénès
2017-03-19Merge PR#487: Add a forgotten (?) line to "theories/Logic/vo.itarget".Maxime Dénès
2017-03-19Add a forgotten (?) line to "theories/Logic/vo.itarget".Matej Kosik
The "theories/Logic/PropExtensionalityFacts.v" file was: - compiled - used in several places but not actually installed. This commit fixes that.
2017-03-17Merge PR#428: Report missing tactic arguments in error messageMaxime Dénès
2017-03-17Merge PR#437: Improve unification debug trace.Maxime Dénès
2017-03-17Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Maxime Dénès
2017-03-17Merge PR#442: Allow interactive editing of Coq.Init.LogicMaxime Dénès
2017-03-17Merge PR#451: Add η principles for sigma typesMaxime Dénès
2017-03-15Attempt to improve error message when "apply in" fail.Hugo Herbelin
- Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390.
2017-03-15Merge PR#267: Proposal for an update of the recommended style in programming ↵Maxime Dénès
Coq.
2017-03-14[safe-string] Enable -safe-string !Emilio Jesus Gallego Arias
We now build Coq with `-safe-string`, which enforces functional use of the `string` datatype. Coq was pretty safe in these regard so only a few tweaks were needed. - coq_makefile: build plugins with -safe-string too. - `names.ml`: we remove `String.copy` uses, as they are not needed.
2017-03-14[safe-string] toolsEmilio Jesus Gallego Arias
No functional changes.
2017-03-14[safe-string] ideEmilio Jesus Gallego Arias
No functional change, one extra copy introduced but it seems hard to avoid.
2017-03-14[safe-string] plugins/extractionEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe-string] ltac/profile_ltacEmilio Jesus Gallego Arias
No functional change, one extra copy introduced but it seems hard to avoid.
2017-03-14[safe_string] toplevel/vernacEmilio Jesus Gallego Arias
No functional changes, only a minor copy on a deprecated output option.
2017-03-14[safe_string] toplevel/coqloopEmilio Jesus Gallego Arias
No functional change, even if we could optimize `blanch_utf8_string` a bit more by using `String.init`.
2017-03-14[safe-string] parsing/cLexerEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] interp/dumpglobEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] library/nameopsEmilio Jesus Gallego Arias
We add a more convenient API to create identifiers from mutable strings. We cannot solve the `String.copy` deprecation problem until we enable `-safe-string`.
2017-03-14[safe_string] kernel/cemitcodesEmilio Jesus Gallego Arias
The `emitcodes` string type was used in both a functional and an imperative way, so we have to handle it with care in order to preserve the previous optimizations and semantics.
2017-03-14[toplevel] Remove unusable option -notopEmilio Jesus Gallego Arias
Maxime points out that -notop cannot be used as the kernel requires all constants to belong into a module. Indeed: ``` $ rlwrap ./bin/coqtop -notop Coq < Definition foo := True. Toplevel input, characters 0-23: > Definition foo := True. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: No session module started (use -top dir) Coq < Module M. Definition foo := True. End M. Module M is defined Coq < Locate foo. Constant If you see this, it's a bug.M.foo (shorter name to refer to it in current context is M.foo) ``` My rationale for the removal is that this kind of incomplete features are often confusing to newcomers ─ it has happened to me many times ─ as it can be seen for example in #397 .
2017-03-14Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoMaxime Dénès
2017-03-14Report missing tactic arguments in error messageTej Chajed
Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
2017-03-14[safe-string] kernel/nativevaluesEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] kernel/term_typingEmilio Jesus Gallego Arias
No functional change, we create the new string beforehand and `id_of_string` will become a noop with `-safe-string`.
2017-03-14[safe-string] lib/miscelaneaEmilio Jesus Gallego Arias
No functional change.js
2017-03-14[safe-string] lib/cUnixEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] lib/cThreadEmilio Jesus Gallego Arias
No functional changes.
2017-03-14Merge PR#438: Fix V7 syntax in refman.Maxime Dénès
2017-03-14Merge PR#412: Remove outdated comment from 2002.Maxime Dénès
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
2017-03-14Merge PR#477: [travis] Basic support for overlays.Maxime Dénès
2017-03-14Merge PR#473: [ci] Document that sudo: false is slowerMaxime Dénès
2017-03-14Merge PR#464: [META] More fixesMaxime Dénès
2017-03-14Merge PR#446: Remove a dead exception catching code.Maxime Dénès
2017-03-14[future] Remove unused parameter greedy.Emilio Jesus Gallego Arias
It was always set to `greedy:true`.
2017-03-14[library] Refactor state handling.Emilio Jesus Gallego Arias
This part of state is critical. We refactor it and make it into a record to ease handling.
2017-03-14[library] Don't recompute path_prefix on unfreeze.Emilio Jesus Gallego Arias
We instead save the current value.
2017-03-13[travis] Basic support for overlays.Emilio Jesus Gallego Arias
We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support.
2017-03-13Remove a dead exception catching code.Théo Zimmermann
The code was assuming that Proofview.tclFOCUS could raise a CList.IndexOutOfRange exception but this isn't the case. The focusing functions already catch this exception and raises an algebraic exception within the tactic mechanism.
2017-03-13Merge PR#456: Proposing improvement to the CI targets for local useMaxime Dénès
2017-03-12Updating core.dbg after ltac moved to plugins directory.Hugo Herbelin
2017-03-10[travis] Make the git_checkout function more reliable.Théo Zimmermann
This commit also documents the behavior of said function; and fix the location of the ssreflect clone to an absolute path (this is now necessary).
2017-03-10[travis] Adding a template file and using it for all targets.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 05:27:41 +0000