| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-09 | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau | |
| 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). | |||
| 2014-09-09 | Merge remote-tracking branch 'jason/win32-improvements' into trunk | Enrico Tassi | |
| 2014-09-09 | Bump CoqSDK revision number | Jason Gross | |
| 2014-09-09 | Add a VERBOSE flag to make-sdk-win32 | Jason Gross | |
| For debugging purposes. | |||
| 2014-09-09 | Minor code style cleanup in make-sdk-win32 | Jason Gross | |
| 2014-09-09 | Support 64-bit cygwin | Jason Gross | |
| 2014-09-09 | Support machines that have a full or nonexistant C drive | Jason Gross | |
| 2014-09-09 | Support environments where `find` is Windows' find | Jason Gross | |
| 2014-09-09 | Displaying genarg tag in idtac. | Pierre-Marie Pédrot | |
| 2014-09-09 | Installer for win improved | Enrico Tassi | |
| - 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 | |||
| 2014-09-09 | IDE: escape popup text (close: 3600) | Enrico Tassi | |
| 2014-09-09 | Load Prelude.vi if not Prelude.vo is found (Close: 3595) | Enrico Tassi | |
| 2014-09-09 | Marshalling errors should be bold and red (should never happen actually) | Enrico Tassi | |
| 2014-09-09 | A marshalling failure does not make a worker `Old | Enrico Tassi | |
| 2014-09-09 | Documenting the new Undo semantics | Enrico Tassi | |
| 2014-09-09 | Back: print subgoals as in 8.4 (Close: 3585) | Enrico Tassi | |
| 2014-09-09 | BackTo not part of the doc when used by emacs | Enrico Tassi | |
| Used to work "by chance". | |||
| 2014-09-09 | Undo: if the ui is coqtop (command line) then Undo is not part of the doc. | Enrico Tassi | |
| 2014-09-09 | Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407) | Enrico Tassi | |
| 2014-09-09 | IDE: disable editable text area underline when -debug | Enrico Tassi | |
| This way a user *can* use coqide with -debug | |||
| 2014-09-09 | toploop plugins taken into account when printing --help (close: 3535) | Enrico Tassi | |
| 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 | |||
| 2014-09-09 | Installer for win32 | Enrico Tassi | |
| 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 | |||
| 2014-09-09 | IDECDEPSFLAGS is for byte, not opt | Enrico Tassi | |
| 2014-09-08 | Fixing TestRefine test-suite file. | Pierre-Marie Pédrot | |
| 2014-09-08 | Removing antiquotations in Tauto. | Pierre-Marie Pédrot | |
| 2014-09-08 | Removing dead code relative to the XML plugin. | Pierre-Marie Pédrot | |
| 2014-09-08 | Removing the documentation of the XML plugin. | Pierre-Marie Pédrot | |
| 2014-09-08 | Removing the XML plugin. | Pierre-Marie Pédrot | |
| Left a README, just in case someone will discover the remnants of it decades from now. | |||
| 2014-09-08 | Fix bug #3591: print differently eta-expanded projection implicit ↵ | Matthieu Sozeau | |
| application and primitive projection when they would otherwise be ambiguous. | |||
| 2014-09-08 | Parsing of Type@{max(i,j)}. | Matthieu Sozeau | |
| 2014-09-08 | Display number of available goals in "incorrect number of goals" error message. | Arnaud Spiwack | |
| 2014-09-08 | CHANGES: existential variables are always "substituted" in the new tactic ↵ | Arnaud Spiwack | |
| engine. | |||
| 2014-09-08 | CHANGES: Ltac's [refine] accepts [uconstr]. | Arnaud Spiwack | |
| 2014-09-08 | Doc: [revgoals]. | Arnaud Spiwack | |
| 2014-09-08 | CHANGES: [revgoals]. | Arnaud Spiwack | |
| 2014-09-08 | Fix [induction] wrt inductive records and non-recursive variants. | Arnaud Spiwack | |
| - [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. | |||
| 2014-09-08 | CHANGES: [Variant], [Set Nonrecursive Elimination Schemes]. | Arnaud Spiwack | |
| 2014-09-08 | CHANGES: binder names from Ltac identifiers. | Arnaud Spiwack | |
| 2014-09-08 | Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context]. | Arnaud Spiwack | |
| 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). | |||
| 2014-09-08 | The [constr:(…)] Ltac construction now shares the same context as ↵ | Arnaud Spiwack | |
| [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]. | |||
| 2014-09-08 | Add a tactic [revgoals] to reverse the list of focused goals. | Arnaud Spiwack | |
| 2014-09-08 | Fix bug #3589, unification looping due to incorrect use of stack with ↵ | Matthieu Sozeau | |
| primitive projections. | |||
| 2014-09-07 | Little fix in documentation of inversion. | Hugo Herbelin | |
| 2014-09-07 | Test for "inversion as" naming bug. | Hugo Herbelin | |
| 2014-09-07 | A better check that an "as" clause has been given to inversion, so | Hugo Herbelin | |
| 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). | |||
| 2014-09-07 | Fixing a bug in intros_replacing which was causing inversion not | Hugo Herbelin | |
| necessarily granting names given in the "as" clause. | |||
| 2014-09-07 | Fixing "simple inversion as" (bug #2164). | Hugo Herbelin | |
| 2014-09-07 | Dead code in inv.ml. | Hugo Herbelin | |
| 2014-09-07 | Regression test #3557 | Hugo Herbelin | |
| 2014-09-07 | Regression test for bug #2883. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |