aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* No plural for only one non existing focused goal.Gravatar Hugo Herbelin2014-09-12
|
* Fix source of initial goal.Gravatar Hugo Herbelin2014-09-12
|
* Commit 682aa67cc80 about enforcing that apply does not create newGravatar Hugo Herbelin2014-09-12
| | | | | evars was too liberal. Using an intermediate criterion which makes both tests apply.v and 3284.v working.
* Discontinued xml plugin: improve the README.Gravatar Arnaud Spiwack2014-09-12
| | | More information, less pmp.
* Replace the list of argument in tacexpr with a single row argument.Gravatar Arnaud Spiwack2014-09-12
| | | | | | This has several benefits * It replicates the "no quadrillion-uple" pattern at the level of types. Giving names to the various component will hopefully make for better error messages. * It is less typo-prone, as the whole row can be passed as an argument rather than retyping each of the arguments. Also makes for a terser [Tacexpr]. * More importantly: local changes to tactic expressions will more often be kept local. Which will avoid some extra tedious work, and make rebases on top of such changes significantly easier.
* Oopps.. fixed the .ml not the .ml4Gravatar Matthieu Sozeau2014-09-11
|
* Use an AST for strategy names.Gravatar Matthieu Sozeau2014-09-11
|
* Fix test-suite files, and move some opened to closed.Gravatar Matthieu Sozeau2014-09-11
|
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
| | | | | | | matching (i.e. no instanciation of the goal evars). Classes defined when [Set Typeclasses Strict Resolution] is on use the restricted resolution for all their instances (except for Hint Extern's).
* Keeping a sub-optimal behavior of intros_possibly_replacing for ↵Gravatar Hugo Herbelin2014-09-11
| | | | compatibility with inversion
* Other bugs with "inversion as" (collision between user-provided names and ↵Gravatar Hugo Herbelin2014-09-11
| | | | generated equation names).
* Fix bug #3594: eta for constructors and functions at the same time whichGravatar Matthieu Sozeau2014-09-11
| | | | | was failing in this case due to the wrong postponment of an unsolvable ?X = RigidContext[?X] problem.
* Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Gravatar Matthieu Sozeau2014-09-11
|
* Fix bug #3505.Gravatar Matthieu Sozeau2014-09-11
| | | | | | | When w_unifying primitive projection applications, force the unification of types of the projected records to recover instances for the parameters (evarconv does this automatically by unifying evar instances with their expected type).
* Fixing bug #3605.Gravatar Pierre-Marie Pédrot2014-09-11
|
* Removing remaining documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-11
|
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
| | | | | | | | | | selection (rewrite, destruct/induction, set or apply on scheme), for unification (apply on not a scheme, auto), the latter being separated into primary unification and unification for merging instances. No change of semantics from within Coq, if I did not mistake (but a function like secondOrderAbstraction does not set flags by itself anymore).
* Parsing and printing of primitive projections, fix buggy behavior whenGravatar Matthieu Sozeau2014-09-10
| | | | implicits do not allow to parse as an application and cleanup code.
* Fix generation of inductive elimination principle for primitive records.Gravatar Matthieu Sozeau2014-09-10
| | | | Let r.(p) be a strict subterm of r during the guardness check.
* Fix categorization of recursive inductives.Gravatar Matthieu Sozeau2014-09-10
|
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
|
* More small bugs in intros_replacing.Gravatar Hugo Herbelin2014-09-10
|
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
| | | | | | | in69665dd2480d364162933972de7ffa955eccab4d. There are still situations when "as" is not given where equations coming from injection are not yet removed, making invalid the computation of dependencies, what prevents an hypothesis to be cleared and replaced.
* Example for apply and evars.Gravatar Hugo Herbelin2014-09-10
|
* Removing "eqn:" for "induction" in reference manual.Gravatar Hugo Herbelin2014-09-10
|
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
|
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
| | | | | | | | Printing All cases (bug #3597). - Fix Ltac matching with primitive projections (bug #3598). - Spotted a problem with printing of constants with maximally implicit arguments due to strange "compatibility" interpretation of Arguments [X] as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
* Merge remote-tracking branch 'jason/win32-improvements' into trunkGravatar Enrico Tassi2014-09-09
|\
| * Bump CoqSDK revision numberGravatar Jason Gross2014-09-09
| |
| * Add a VERBOSE flag to make-sdk-win32Gravatar Jason Gross2014-09-09
| | | | | | | | For debugging purposes.
| * Minor code style cleanup in make-sdk-win32Gravatar Jason Gross2014-09-09
| |
| * Support 64-bit cygwinGravatar Jason Gross2014-09-09
| |
| * Support machines that have a full or nonexistant C driveGravatar Jason Gross2014-09-09
| |
| * Support environments where `find` is Windows' findGravatar Jason Gross2014-09-09
| |
* | Displaying genarg tag in idtac.Gravatar Pierre-Marie Pédrot2014-09-09
| |
* | Installer for win improvedGravatar Enrico Tassi2014-09-09
|/ | | | | | | | | - checks for paths containing whitespaces - Coqide has syntax highlighting - does not include the ocaml compiler, since it would not work anyway for the purpose of native compile. For that we really need the whole toolchain, including the C linker/assembler. Hence we should just recommend to install the SDK
* IDE: escape popup text (close: 3600)Gravatar Enrico Tassi2014-09-09
|
* Load Prelude.vi if not Prelude.vo is found (Close: 3595)Gravatar Enrico Tassi2014-09-09
|
* Marshalling errors should be bold and red (should never happen actually)Gravatar Enrico Tassi2014-09-09
|
* A marshalling failure does not make a worker `OldGravatar Enrico Tassi2014-09-09
|
* Documenting the new Undo semanticsGravatar Enrico Tassi2014-09-09
|
* Back: print subgoals as in 8.4 (Close: 3585)Gravatar Enrico Tassi2014-09-09
|
* BackTo not part of the doc when used by emacsGravatar Enrico Tassi2014-09-09
| | | | Used to work "by chance".
* Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Gravatar Enrico Tassi2014-09-09
|
* Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Gravatar Enrico Tassi2014-09-09
|
* IDE: disable editable text area underline when -debugGravatar Enrico Tassi2014-09-09
| | | | This way a user *can* use coqide with -debug
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
| | | | | | | | | | | | | E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE
* Installer for win32Gravatar Enrico Tassi2014-09-09
| | | | | | | | | | | | Not 100% functional, but coqide works. The native compiler is embedded but: - some path mangling problem prevents it from working even when run via cygwin (like in the build process) - CAMLLIB must be exported to ${COQ}\ocaml\lib to have it run (coq should do it). fix
* IDECDEPSFLAGS is for byte, not optGravatar Enrico Tassi2014-09-09
|
* Fixing TestRefine test-suite file.Gravatar Pierre-Marie Pédrot2014-09-08
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 02:37:27 +0000