aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-07-16Added abstration layer to goal display in CoqIDE, and cleaned partsppedrot
of the code altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15623 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-16Fixing goal display when still focussing but no more goals.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15622 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-13Display the "unjustified" information returned by coqtop.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15620 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-13Fixes r15610 (A new status Unsafe in Interface).aspiwack
Two warnings had passed my sensors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15619 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12flex_maybeflex factoringpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15618 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12miller_pfenning unification code factoringpboutill
Mind that the behavior of MaybeFlexible, Flexible changes \! (we solve_pattern_eqn using the new list and not the old one) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15617 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12flex_kind_of_term does not have a copy of termpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15616 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12evar reduction is already made by whd_*pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15615 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12tacred uses stack_reduction_function instead of state_reduction_functionpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15614 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12A new status Unsafe in Interface. Meant for commands such as Admitted.aspiwack
Currently : - only Admitted uses the Unsafe return status - the status is ignored in coqtop - Coqide sees the status but apparently doesn't use it for colouring (I'm not sure why, but then again, it's not as if I understood coqide's code or anything) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15610 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797)letouzey
If an EXTEND block triggers an exception, the current behavior is to print the exception (with Errors.print) ... and continue as if nothing happened. It's tempting to stop ignoring this exception, but that would currently break ssreflect. For the moment, we simply display a nicer message as suggested in bug #2797: - the message starts with Warning instead of Error, and ends with a \n - it also embeds the name of the concerned EXTEND block git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15607 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12Ensure that a plugin init function is called only onceletouzey
In particular restoring a frozen summary (for instance during a backtrack) will not replay the plugin init functions. Backtracking on a "Declare ML Module" and replaying it will correctly replay the init function (cache function in libobject). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15606 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12Vernacentries: minor code cleanupletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15605 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12Bug 2838: ExplApp in mutual inductive parameterspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15604 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfindpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15603 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-11Set/Unset Atomic Load : a pragmatic solution for part 2 of #2820letouzey
This provides an ad-hoc way to solve the second part of bug #2820 (Show Script not working when proof started inside a Load) When doing Load on a file, two behaviors are possible: - either the history stack is grown by only one command, the "Load" itself. This is mandatory for command-counting interfaces (CoqIDE). - either each individual sub-commands in the file is added to the history stack. This allows commands like Show Script to work across the loaded file boundary (cf. bug #2820). Ideally, we should be able to combine someday the benefits of the two approaches. But in the meantime, we resort to a flag : using "Unset Atomic Load" should make "Show Script" work across Load. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15601 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-11Also allow Reset in Load'ed filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15599 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-11Re-allow Reset in compiled filesletouzey
This was a wish by A. Chlipala on coq-club Both Reset foo and Reset Initial are accepted (with a warning). If some proofs were opened, all of them are aborted. This isn't the behavior of the interactive Reset that has more information and can be more selective, but this shouldn't be a big issue in practice. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15597 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-11Severe reorganisation of the code of tactics in Proofview.aspiwack
All the purely monadic code has been moved to a new module Monads, where, I'm afraid to confess, I got to use a number of proof transformers to modularise the definition of tactics. It is still not easy to understand (why would it with backtracking support?) but at least it's more robust, cleaner, and more extensible. Plus there is now a Proofview.tclORELSE which will be used to interprete the Ltac tactical (t1 || t2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15596 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-11Fix regression introduced in r15418 that broke MathClasses. In program mode, ↵msozeau
try program coercions before the last resort typeclass resolution to resolve a conversion problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15595 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-11Fix typeclass error handling which was sometimes raising a Failure ("hd").msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15593 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-11A friendlier printing of remaining goals when no goal is focused.aspiwack
Only their conclusion is printed (with a "subgoal n" header) like every goal but the first in the usual case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15591 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Fixing Print Assumption displayppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15590 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Restore test file induct.v where the "in |- *" is mandatoryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15585 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10isolate instances about Permutation and PermutationA which may slow rewriteletouzey
After discovering a rewrite in Ergo that takes a loooong time due to a bad interaction with the instances of Permutation and PermutationA : - PermutationA is now in a separate file SetoidPermutation - File Permutation.v isn't Require'd by SetoidList anymore nor MergeSort.v, just the definitions in Sorted.v - Attempt to put a priority on these instances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Better treatment of error messages in rewrite (avoid use of Errors.print).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15583 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Adapting the IDE interface with the focussed display.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15579 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Small change in the printing of proofs for use by coqide.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15577 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Fixes bug 2841 ([Focus 0] gives anomaly).aspiwack
Now a proper error message is displayed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15574 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Another correction to the dependent existential variable printingaspiwack
for emacs mode. Hopefully fixes Bug 2678 this time. Much saner and more compact code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15573 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09destruct: full compatibility with former _eqn syntaxletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15571 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09Moved code out of ide_slave in a more appropriate place.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15570 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09The tactic remember now accepts a final eqn:H option (grant wish #2489)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15567 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
The ugly syntax "destruct x as [ ]_eqn:H" is replaced by: destruct x eqn:H destruct x as [ ] eqn:H Some with induction. Of course, the pattern behind "as" is arbitrary. For an anonymous version, H could be replaced by ?. The old syntax with "_eqn" still works for the moment, by triggers a warning. For making this new syntax work, we had to change the seldom-used "induction x y z using foo" into "induction x, y, z using foo". Now, only one "using" can be used per command instead of one per comma-separated group earlier, but I doubt this will bother anyone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09Avoid a warning about unprintable new command Print Namespaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15565 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09Fixed fake_ide test-suite.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15564 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-08verbose compat notations : nicer option nameletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15548 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-07Restore an indentation of Show Scriptletouzey
Based on a patch contributed by D. de Rauglaudre on coq-dev. I've added some specific treatment of { } and bullets - + *. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15546 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-07Ring_polynom : a restricted simpl instead of a unfold;foldletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15545 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Continuing r15459: it helps testing occur-check early in someherbelin
situations (see rewrite MonoidMonadTrans.bind_toLower' in Misc/QuicksortComplexity/monoid_expec.v). Also fixing badly designed test 2817.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15543 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Minor fixes in the test-suite after my recent commitsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15542 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Two adaptations after the changes of level of ->letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15541 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06BinPos/BinInt/BinNat : fix some argument scopesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15540 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Restore the compatibility notation Compare.not_eq_symletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15539 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Fix order of introduction of hints to preserve most-recent-first semantics.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15538 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06A prototype implementation of a Print Namespace command.aspiwack
It is used as Print Namespace Coq.Init. This prototypes only prints the name of constants (hence no inductive types). The display order is a tad arbitrary too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15537 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Fixes a bug in the parsing of the grammar entry dirpath which would,aspiwack
amusingly, show up when writing dir path of length at least 3 (with Print LoadPath). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15536 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Practical fix for bug #1206 (anomaly raised in pretyping instead ofherbelin
error when called on ill-typed term, because pretyping called retyping which in turn is expected to be called only with typable arguments). Incidentally, #1206 shows once more time the problem of confusion between section variables (which morally don't have to be cleared) and their copy in goal (which can be cleared). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15533 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Fixes bug #2678aspiwack
Some "dependent evars" were forgotten in the emacs mode. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15530 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Backtrack: add support for the "Proof c." syntax (fix #2832)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15528 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:50:24 +0000