| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-09-07 | Fixing bug #3492. | Pierre-Marie Pédrot | |
| 2014-09-06 | Inlining code in Tacinterp that was only used once. | Pierre-Marie Pédrot | |
| 2014-09-06 | Code simplification in Tacinterp. | Pierre-Marie Pédrot | |
| 2014-09-06 | Proper interpretation function for tauto. | Pierre-Marie Pédrot | |
| Instead of passing glob tactics through the infamous globTacticIn hack and antiquotation feature of the Ltac syntax, we put them in the interpretation environment as closures. This should be used everywhere to get rid of this buggy antiquotation syntax. This fixes bug #2800. | |||
| 2014-09-06 | Adding a way to inject tactic closures in interpretation values. | Pierre-Marie Pédrot | |
| 2014-09-06 | Fixing clearbody : typecheck definitions in context. | Pierre-Marie Pédrot | |
| 2014-09-06 | Renaming goal-entering functions. | Pierre-Marie Pédrot | |
| 1. Proofview.Goal.enter into Proofview.Goal.nf_enter. 2. Proofview.Goal.raw_enter into Proofview.Goal.enter. 3. Proofview.Goal.goals -> Proofview.Goals.nf_goals 4. Proofview.Goal.raw_goals -> Proofview.Goals.goals 5. Ftactic.goals -> Ftactic.nf_goals 6. Ftactic.raw_goals -> Ftactic.goals This is more uniform with the other functions of Coq. | |||
| 2014-09-06 | Fix bug #3584, elaborating pattern-matching on primitive records to the | Matthieu Sozeau | |
| use of projections. | |||
| 2014-09-06 | Remove debug printing code | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |