| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-11 | Fix bug #3505. | Matthieu Sozeau | |
| 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). | |||
| 2014-09-11 | Fixing bug #3605. | Pierre-Marie Pédrot | |
| 2014-09-11 | Removing remaining documentation of the XML plugin. | Pierre-Marie Pédrot | |
| 2014-09-10 | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin | |
| 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). | |||
| 2014-09-10 | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau | |
| implicits do not allow to parse as an application and cleanup code. | |||
| 2014-09-10 | Fix generation of inductive elimination principle for primitive records. | Matthieu Sozeau | |
| Let r.(p) be a strict subterm of r during the guardness check. | |||
| 2014-09-10 | Fix categorization of recursive inductives. | Matthieu Sozeau | |
| 2014-09-10 | Fixing localisation of tactic errors (my mistake in himsg.ml essentially). | Hugo Herbelin | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |