| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-03-22 | Aliasing give_up with admit | Enrico Tassi | |
| 2015-03-22 | STM: if Set Universe Polymorphism then synchronous (#4119) | Enrico Tassi | |
| It was detecting only the per-lemma Polymorphic flag, but not the global one. | |||
| 2015-03-22 | STM: do not delegate proofs containing Print | Enrico Tassi | |
| 2015-03-22 | STM: after every command restore the expected proof mode | Enrico Tassi | |
| 2015-03-22 | typo | Enrico Tassi | |
| 2015-03-21 | Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107) | Guillaume Melquiond | |
| 2015-03-21 | Avoid segfault from code extracted to ghc. (Fix for bug #1257) | Guillaume Melquiond | |
| 2015-03-21 | Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221) | Guillaume Melquiond | |
| 2015-03-21 | Do not revert parameter lists when extracting singleton types to Haskell. ↵ | Guillaume Melquiond | |
| (Fix for bugs #3470 and #3694) | |||
| 2015-03-20 | Fixed #4138. In emacs mode Set/Unset does not print the goal anymore. | Pierre Courtieu | |
| In PG there are shortcuts that perform on the fly "Set Printing All"/"Unset Printing All" in pg. For example if you type C-u before some shortcut for print (check/About/Show), it performs: Set Printing All. Print foo. Unset Printing All. But if the "Unset" prints a goal, then pg interprets the output of Print as a command applied on a previous line, and thus hides it. So for emacs mode I would prefer no goal printing when options are set/unset. In the situation where this should be done (when setting durably the option probably), I'd rather program a "Show" explicitely. | |||
| 2015-03-18 | More sharing in module substitution. | Pierre-Marie Pédrot | |
| 2015-03-18 | add -type-in-type to the usage message | Daniel R. Grayson | |
| 2015-03-18 | Fixing internal representation of Dyn.t in votour. | Pierre-Marie Pédrot | |
| 2015-03-17 | Add function to fix the non-substituted universe variables of an evar_map. | Matthieu Sozeau | |
| 2015-03-16 | Removing the whole library content from the summary. | Pierre-Marie Pédrot | |
| It is still present in the libstack, though. | |||
| 2015-03-16 | More invariants in Library. | Pierre-Marie Pédrot | |
| We explicit the fact that we only need the name of the library in most of the summaries. | |||
| 2015-03-16 | gitattributes: add `.mailmap` file to the list of files excluded from the ↵ | Arnaud Spiwack | |
| `.tar.gz`. | |||
| 2015-03-16 | Gitattributes file added to generate archive. | Guillaume Claret | |
| Cherry-picked from v8.4 ( c1aabb104122ead02fa289339a42815373338222 ). | |||
| 2015-03-16 | Adding a primitive to dump the current association table of dynamic types. | Pierre-Marie Pédrot | |
| 2015-03-15 | STM: -debug: better explanation of why not async (#4125) | Enrico Tassi | |
| 2015-03-15 | STM: -quick: async no Proof using but no Section (#4124) | Enrico Tassi | |
| As happens in interactive mode. | |||
| 2015-03-14 | End of Bug 3986 - make cleanall removes .*.aux files | Pierre Boutillier | |
| 2015-03-14 | Bug 3981 ends to convice me that subdirs in coq_makefile deverse a warning | Pierre Boutillier | |
| 2015-03-14 | Fix Bug 3548 - Makefile should fallback gracefully in the absence of codesign | Pierre Boutillier | |
| 2015-03-13 | Fix compilation with forthcoming Ocaml version 4.03. | Arnaud Spiwack | |
| Backported from a patch for v8.4 by Pierre Chambart. Part of the commit has been rendered obsolete by code reorganisation, leaving: * OCaml runtime header files used to declare the int32, uint32, int64 and uint64 type. That got removed, and uses of those types should be replaced by the standard ones: uint32_t, int32_t, int64_t, uint64_t. Those are defined in stdint.h. | |||
| 2015-03-13 | Declarative mode: make it so that unfocussing can only be done for closed ↵ | Arnaud Spiwack | |
| subproofs. The front-end is supposed to take care of that, but it may help to catch bugs. | |||
| 2015-03-13 | Declarative mode: remove dead code. | Arnaud Spiwack | |
| 2015-03-13 | Declarative mode: remove a superfluous [set_proof_mode]. | Arnaud Spiwack | |
| It was probably creating bugs when trying to use [escape]. | |||
| 2015-03-13 | Declarative mode: fix the focus behaviour. | Arnaud Spiwack | |
| I had previously mistakenly enforced the property that after solving every goal in a block, unfocusing was performed automatically until one goal is in focus. This is not how the declarative mode is supposed to behave. Rather every focus must be explicitely unfocused by a closing command. This hit a few bad interaction with the pure representation of proof introduced for the asynchronous processing. Some of the invariants seem fragile, so this minimally disruptive solution is probably not long-term. In particular since each block uses the same focus kind, an `end <block>` may close another block than intended if the number of unfocussing command executed is not the right one. | |||
| 2015-03-13 | rewiring Czar printers that were disabled | Pierre Corbineau | |
| Backported from trunk. | |||
| 2015-03-13 | CHANGES: more correct equivalent to "constructor tac" syntax. | Arnaud Spiwack | |
| As mentionne in #3969, using "once (constructor;tac)" leads in exponential blowups, whereas "[> once (constructor;tac) ..]" does not. | |||
| 2015-03-13 | Add some tests for tryif | Jason Gross | |
| + adjusting for the removal of `admit` by Arnaud Spiwack. | |||
| 2015-03-13 | Fixing #4127 (command for locating exists notation in refman changed). | Hugo Herbelin | |
| 2015-03-12 | Fixing bug #4055. | Pierre-Marie Pédrot | |
| When lauching ideslave without configuring the communication channels, instead of raising an anomaly which is never caught by the main loop, we rather exit the process with a relevant error message. | |||
| 2015-03-11 | Fix double print in decl_mode. | Enrico Tassi | |
| After executing a command classified as VtProofStep the stm prints the goals (if used via the tty API). | |||
| 2015-03-11 | Fix regression in HoTT_coq_014.v | Enrico Tassi | |
| Admitted was not using the partial proof to infer discharged variables. Now it does. The fix makes no sense, but restore the old behavior. | |||
| 2015-03-11 | CoqIDE: load first _CoqProject file found and notify the user | Enrico Tassi | |
| 2015-03-11 | CoqIDE: fix tag colors to support superposing unsafe and partial | Enrico Tassi | |
| Admitted (like Qed) can be "partially executed", but is also unsafe. | |||
| 2015-03-11 | CoqIDE: restore module/proof name in info bar | Enrico Tassi | |
| 2015-03-11 | CoqIDE: do not lose tag on Qed ending focused proof | Enrico Tassi | |
| 2015-03-11 | STM: ease re-editing of Admitted proofs | Enrico Tassi | |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | |
| - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit | |||
| 2015-03-09 | Do not display the status of monomorphic constants unless in ↵ | Guillaume Melquiond | |
| universe-polymorphism mode. | |||
| 2015-03-08 | Test for bug #2951. | Pierre-Marie Pédrot | |
| 2015-03-08 | Fixing bug #2951. | Pierre-Marie Pédrot | |
| 2015-03-07 | Test for #4035 (dependent destruction from Ltac). | Hugo Herbelin | |
| 2015-03-07 | Reverting r10021 which enforces early assumptions on freshness which | Hugo Herbelin | |
| seem to be overly strong in practice (see discussion related to #4035). | |||
| 2015-03-07 | Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar". | Hugo Herbelin | |
| Not inventing a new fresh name if a non-fresh name is explicitly given, as in v8.4. | |||
| 2015-03-06 | Add some missing Proof keywords. | Guillaume Melquiond | |
| 2015-03-06 | Simplify grammar for syntax highlighting by removing extraneous parentheses. | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |