| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-10 | More small bugs in intros_replacing. | Hugo Herbelin | |
| 2014-09-10 | Fixing inversion after having fixed intros_replacing | Hugo Herbelin | |
| 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. | |||
| 2014-09-10 | Example for apply and evars. | Hugo Herbelin | |
| 2014-09-10 | Removing "eqn:" for "induction" in reference manual. | Hugo Herbelin | |
| 2014-09-10 | VernacExtend does not dispatch on type anymore. | Pierre-Marie Pédrot | |
| 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). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |