aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* A new status Unsafe in Interface. Meant for commands such as Admitted.Gravatar aspiwack2012-07-12
| | | | | | | | | | | 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
* Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797)Gravatar letouzey2012-07-12
| | | | | | | | | | | | | | 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
* Ensure that a plugin init function is called only onceGravatar letouzey2012-07-12
| | | | | | | | | | 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
* Vernacentries: minor code cleanupGravatar letouzey2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2838: ExplApp in mutual inductive parametersGravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfindGravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Set/Unset Atomic Load : a pragmatic solution for part 2 of #2820Gravatar letouzey2012-07-11
| | | | | | | | | | | | | | | | | | | 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
* Also allow Reset in Load'ed filesGravatar letouzey2012-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15599 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-allow Reset in compiled filesGravatar letouzey2012-07-11
| | | | | | | | | | | 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
* Severe reorganisation of the code of tactics in Proofview.Gravatar aspiwack2012-07-11
| | | | | | | | | | | 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
* Fix regression introduced in r15418 that broke MathClasses. In program mode, ↵Gravatar msozeau2012-07-11
| | | | | | | | | 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
* Fix typeclass error handling which was sometimes raising a Failure ("hd").Gravatar msozeau2012-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15593 85f007b7-540e-0410-9357-904b9bb8a0f7
* A friendlier printing of remaining goals when no goal is focused.Gravatar aspiwack2012-07-11
| | | | | | | 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
* Fixing Print Assumption displayGravatar ppedrot2012-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore test file induct.v where the "in |- *" is mandatoryGravatar letouzey2012-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15585 85f007b7-540e-0410-9357-904b9bb8a0f7
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
| | | | | | | | | | | | 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
* Better treatment of error messages in rewrite (avoid use of Errors.print).Gravatar msozeau2012-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adapting the IDE interface with the focussed display.Gravatar ppedrot2012-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small change in the printing of proofs for use by coqide.Gravatar aspiwack2012-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes bug 2841 ([Focus 0] gives anomaly).Gravatar aspiwack2012-07-10
| | | | | | 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
* Another correction to the dependent existential variable printingGravatar aspiwack2012-07-10
| | | | | | | | 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
* destruct: full compatibility with former _eqn syntaxGravatar letouzey2012-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved code out of ide_slave in a more appropriate place.Gravatar ppedrot2012-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15570 85f007b7-540e-0410-9357-904b9bb8a0f7
* The tactic remember now accepts a final eqn:H option (grant wish #2489)Gravatar letouzey2012-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15567 85f007b7-540e-0410-9357-904b9bb8a0f7
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
| | | | | | | | | | | | | | | | | | 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
* Avoid a warning about unprintable new command Print NamespaceGravatar letouzey2012-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15565 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed fake_ide test-suite.Gravatar ppedrot2012-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15564 85f007b7-540e-0410-9357-904b9bb8a0f7
* verbose compat notations : nicer option nameGravatar letouzey2012-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15548 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore an indentation of Show ScriptGravatar letouzey2012-07-07
| | | | | | | 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
* Ring_polynom : a restricted simpl instead of a unfold;foldGravatar letouzey2012-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r15459: it helps testing occur-check early in someGravatar herbelin2012-07-06
| | | | | | | | | 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
* Minor fixes in the test-suite after my recent commitsGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15542 85f007b7-540e-0410-9357-904b9bb8a0f7
* Two adaptations after the changes of level of ->Gravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15541 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinPos/BinInt/BinNat : fix some argument scopesGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15540 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore the compatibility notation Compare.not_eq_symGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix order of introduction of hints to preserve most-recent-first semantics.Gravatar msozeau2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15538 85f007b7-540e-0410-9357-904b9bb8a0f7
* A prototype implementation of a Print Namespace command.Gravatar aspiwack2012-07-06
| | | | | | | | | 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
* Fixes a bug in the parsing of the grammar entry dirpath which would,Gravatar aspiwack2012-07-06
| | | | | | | 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
* Practical fix for bug #1206 (anomaly raised in pretyping instead ofGravatar herbelin2012-07-06
| | | | | | | | | | | 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
* Fixes bug #2678Gravatar aspiwack2012-07-06
| | | | | | 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
* Backtrack: add support for the "Proof c." syntax (fix #2832)Gravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15528 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)Gravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15525 85f007b7-540e-0410-9357-904b9bb8a0f7
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
| | | | | | | | | One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick update to CHANGES, mention especially the new parsing of ->Gravatar letouzey2012-07-05
| | | | | | | | | | | | | | | So -> is at level 99 since commit 15515. In particular it has now *less* priority than <->, i.e. A->B<->C is now parsed as A->(B<->C) instead of the former awkward and beginner-misleading (A->B)<->C. Sorry, I was planning to do a separate commit for that, but I forgot. In fact, the parsing rules for -> were slightly changed during Pierre B's recent conversion of -> to a true Notation, leading to a nasty sitution : A->B<->C->D was parsed as A->(B<->(C->D)). With no obvious solution to restore full compatibility, we decided to go for the parsing described above, both easy to implement and to work with. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15523 85f007b7-540e-0410-9357-904b9bb8a0f7
* rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteGravatar letouzey2012-07-05
| | | | | | | | | | | rewrite_db fails if nothing has been rewritten, and it only performs *one* top-down pass. For the moment, use (repeat rewrite_db) for emulating more closely autorewrite. Btw, let's make Himsg.explain_ltac_call_trace robust wrt TacExtend with fun(ny) parts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15522 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleanup in Ring_polynom and EnvRingGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15521 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some cleanup in recent proofs concerning piGravatar letouzey2012-07-05
| | | | | | | | Initial idea was to just avoid compat notations such as Z_of_nat --> Z.of_nat, but I ended trying to improve a few proofs... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15520 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetRBT : elementary arith proofs instead of calls to liaGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15519 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 02:51:51 +0000