aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* - 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
|
* Removing antiquotations in Tauto.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Removing the documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
| | | | | Left a README, just in case someone will discover the remnants of it decades from now.
* Fix bug #3591: print differently eta-expanded projection implicit ↵Gravatar Matthieu Sozeau2014-09-08
| | | | | | application and primitive projection when they would otherwise be ambiguous.
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
|
* Display number of available goals in "incorrect number of goals" error message.Gravatar Arnaud Spiwack2014-09-08
|
* CHANGES: existential variables are always "substituted" in the new tactic ↵Gravatar Arnaud Spiwack2014-09-08
| | | | engine.
* CHANGES: Ltac's [refine] accepts [uconstr].Gravatar Arnaud Spiwack2014-09-08
|
* Doc: [revgoals].Gravatar Arnaud Spiwack2014-09-08
|
* CHANGES: [revgoals].Gravatar Arnaud Spiwack2014-09-08
|
* Fix [induction] wrt inductive records and non-recursive variants.Gravatar Arnaud Spiwack2014-09-08
| | | | - [induction] on inductive records use the generated induction scheme for induction (not destruct as for non-recursive records) - [induction] on non-recursive variants do destruct as the induction scheme is not generated.
* CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].Gravatar Arnaud Spiwack2014-09-08
|
* CHANGES: binder names from Ltac identifiers.Gravatar Arnaud Spiwack2014-09-08
|
* Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].Gravatar Arnaud Spiwack2014-09-08
| | | The latter is more representative of its actual function: extract from the Ltac context the values which are relevant to the interpretation of terms (either type or untyped).
* The [constr:(…)] Ltac construction now shares the same context as ↵Gravatar Arnaud Spiwack2014-09-08
| | | | | | [uconstr:(…)]. - The binders names can be influenced by binders defined in Ltac (e.g. [let x:=fresh"y" in let u:=constr:(fun x:nat=>x) in idtac u] ). - Any untyped constr in the context can now be inserted and type-checked inside a constr. In particular, Gregory Malecha's original proposed syntax for type-checking untyped terms in Ltac is now available [let u:=uconstr:(I I) in let v := constr:(u) in idtac v].
* Add a tactic [revgoals] to reverse the list of focused goals.Gravatar Arnaud Spiwack2014-09-08
|
* Fix bug #3589, unification looping due to incorrect use of stack with ↵Gravatar Matthieu Sozeau2014-09-08
| | | | primitive projections.
* Little fix in documentation of inversion.Gravatar Hugo Herbelin2014-09-07
|
* Test for "inversion as" naming bug.Gravatar Hugo Herbelin2014-09-07
|
* A better check that an "as" clause has been given to inversion, soGravatar Hugo Herbelin2014-09-07
| | | | | | | that it clears things earlier in the "as" case, allowing intros_replacing to work without renaming the hypotheses. (clear_request was not a good idea here a priori, since its use was not related to the hypothesis to invert but to an hypothesis to inject).
* Fixing a bug in intros_replacing which was causing inversion notGravatar Hugo Herbelin2014-09-07
| | | | necessarily granting names given in the "as" clause.
* Fixing "simple inversion as" (bug #2164).Gravatar Hugo Herbelin2014-09-07
|
* Dead code in inv.ml.Gravatar Hugo Herbelin2014-09-07
|
* Regression test #3557Gravatar Hugo Herbelin2014-09-07
|
* Regression test for bug #2883.Gravatar Hugo Herbelin2014-09-07
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 14:26:44 +0000