aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fix compilation with forthcoming Ocaml version 4.03.Gravatar Arnaud Spiwack2015-03-13
| | | | | | | 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.
* Declarative mode: make it so that unfocussing can only be done for closed ↵Gravatar Arnaud Spiwack2015-03-13
| | | | | | subproofs. The front-end is supposed to take care of that, but it may help to catch bugs.
* Declarative mode: remove dead code.Gravatar Arnaud Spiwack2015-03-13
|
* Declarative mode: remove a superfluous [set_proof_mode].Gravatar Arnaud Spiwack2015-03-13
| | | | It was probably creating bugs when trying to use [escape].
* Declarative mode: fix the focus behaviour.Gravatar Arnaud Spiwack2015-03-13
| | | | | | | | 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.
* rewiring Czar printers that were disabledGravatar Pierre Corbineau2015-03-13
| | | | Backported from trunk.
* CHANGES: more correct equivalent to "constructor tac" syntax.Gravatar Arnaud Spiwack2015-03-13
| | | | As mentionne in #3969, using "once (constructor;tac)" leads in exponential blowups, whereas "[> once (constructor;tac) ..]" does not.
* Add some tests for tryifGravatar Jason Gross2015-03-13
| | | | + adjusting for the removal of `admit` by Arnaud Spiwack.
* Fixing #4127 (command for locating exists notation in refman changed).Gravatar Hugo Herbelin2015-03-13
|
* Fixing bug #4055.Gravatar Pierre-Marie Pédrot2015-03-12
| | | | | | 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.
* Fix double print in decl_mode.Gravatar Enrico Tassi2015-03-11
| | | | | After executing a command classified as VtProofStep the stm prints the goals (if used via the tty API).
* Fix regression in HoTT_coq_014.vGravatar Enrico Tassi2015-03-11
| | | | | Admitted was not using the partial proof to infer discharged variables. Now it does. The fix makes no sense, but restore the old behavior.
* CoqIDE: load first _CoqProject file found and notify the userGravatar Enrico Tassi2015-03-11
|
* CoqIDE: fix tag colors to support superposing unsafe and partialGravatar Enrico Tassi2015-03-11
| | | | Admitted (like Qed) can be "partially executed", but is also unsafe.
* CoqIDE: restore module/proof name in info barGravatar Enrico Tassi2015-03-11
|
* CoqIDE: do not lose tag on Qed ending focused proofGravatar Enrico Tassi2015-03-11
|
* STM: ease re-editing of Admitted proofsGravatar Enrico Tassi2015-03-11
|
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| | | | | | | | | | | | | | | - 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
* Do not display the status of monomorphic constants unless in ↵Gravatar Guillaume Melquiond2015-03-09
| | | | universe-polymorphism mode.
* Test for bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
|
* Fixing bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
|
* Test for #4035 (dependent destruction from Ltac).Gravatar Hugo Herbelin2015-03-07
|
* Reverting r10021 which enforces early assumptions on freshness whichGravatar Hugo Herbelin2015-03-07
| | | | seem to be overly strong in practice (see discussion related to #4035).
* Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".Gravatar Hugo Herbelin2015-03-07
| | | | | Not inventing a new fresh name if a non-fresh name is explicitly given, as in v8.4.
* Add some missing Proof keywords.Gravatar Guillaume Melquiond2015-03-06
|
* Simplify grammar for syntax highlighting by removing extraneous parentheses.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Print/Reset Extraction.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Extraction Inline and add Separate Extraction.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Extraction Language.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Typeclasses Opaque.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Module (Type).Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Extract Inductive.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for Declare Module.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Import and Export.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for Declare ML Module.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Require.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Scheme.Gravatar Guillaume Melquiond2015-03-06
|
* Do not highlight "using" as a constr keyword.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for About.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Save.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for Coercion.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of "Require multiple libraries".Gravatar Guillaume Melquiond2015-03-06
|
* MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
|
* Fix testsuite with respect to the new formatting of Fail messages.Gravatar Guillaume Melquiond2015-03-05
|
* Preprend Fail to all the expected failures in the documentation.Gravatar Guillaume Melquiond2015-03-05
| | | | | | | This commit also removes comments from Coq examples, as they cause extraneous delayed prompts that clutter the output because coq_tex cannot remove them. Some documentation errors were also fixed in the process, since they are easier to spot now that only unexpected failures stand out.
* Do not prepend a "Error:" header when the error is expected by the user.Gravatar Guillaume Melquiond2015-03-05
| | | | | This commit also removes the extraneous "=>" token from Fail messages and prevents them from losing all the formatting information.
* MMaps again : adding MMapList, an implementation by ordered listGravatar Pierre Letouzey2015-03-05
|
* Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
| | | | | | | | | | | | | | | | | | | | | | NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty".
* Fix bug #3532, providing universe inconsistency information when aGravatar Matthieu Sozeau2015-03-04
| | | | unification fails due to that, during a conversion step.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 18:28:41 +0000