aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Open Scope can now also accepts delimiters (e.g. Z).letouzey
Of course, scope names (e.g. Z_scope) are still accepted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15516 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Fixes in rewriting by strategies (almost ready to be documented!):msozeau
- Proper parsing/globalization of strategy expressions. - Correct the error handling that gave rise to anomalies. - More informative error messages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15513 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-04Fixes a bug in Ppvernac which had braces and bullets printed with an endingaspiwack
period. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15509 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-04Change how the number of open goals is printed.aspiwack
If you are focused on 3 subgoals, and unfocusing would reveal 2 extra subgoals, and unfocusing again would reveal 4 extra subgoals, then coqtop will tell you: 3 focused subgoals (unfocused: 2-4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15508 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-04When focused on an empty list of goal (after finishing a subproof introducedaspiwack
by a bullet or a brace, for instance), the message "This subproof is complete […]" is now rendered before the list of goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15507 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Various small display improvementppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15505 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Reversed message display order in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15504 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Small improvement to ide_slave, which was going crazy wheneverppedrot
stdin was accidentaly closed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15503 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Fixing fake_ideppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15502 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Now CoqIDE separates answer and messages. This should hopefullyppedrot
be backward compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-28Cleaning opening of the standard List module.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15500 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-28Replace nat indices with positive one in Btauto.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15499 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-28Fixing previous commit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15498 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-28Fixing info_auto / info_trivial display.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15497 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Added the show_margin_right option to CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15496 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Fixing awkward copy & paste mechanism in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15495 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Now CoqIDE auto-sets the printing width of the goal display.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15494 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Fixed string width printing in string_of_ppcmdsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15493 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Added a Deque module to CLib (to be used in CoqIDE).ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15492 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-25Small code compaction and factoring in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15491 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-25Added a .mli to pretyping/program.mlppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15490 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-24Cosmetic changesppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15489 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-24Made the message view of CoqIDE abstract.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15488 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Documentation of pp.mlippedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15487 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Moving logging level to Interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15486 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Fixed cursor reset in CoqIDE backtrack.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15485 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Factorized bactracking code in CoqIDE. This fixes bug #2821 btw.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15484 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Fixing a potential bug of coqtop management in CoqIDE due to appedrot
careless exception catching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15483 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Fixing Camlp4 compilation (hopefully, preprocessing fixpoint reached...)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15482 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Fixing camlp4 compilation w.r.t previous commitppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15481 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Coq_makefile: make uninstall targetpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15480 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Install is rather beautifulpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15479 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22inthe middle one more timepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15478 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Refactoring seems OKpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15477 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Coq_makefile: separate finding what to install where from generating the ↵pboutill
script that install git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15476 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22I forgot a line in previous commit.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15473 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22A call to the command Proof (and its variants) now prints the subgoals.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15472 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-21Fixed #2821.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15471 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-21Fixing #2825.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15469 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-21Fix bug #2808: wrong handling of evars in Instance command.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15468 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-21Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:msozeau
take care of checking progress when solving the remaining problems, distinguishing between solved and stuck conversions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15467 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-21Fixing accelerator dynamic modification in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15465 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-20Fixing use of an error instead of a boolean result in the unificationherbelin
subroutine choose_less_dependent_instance. This might solve bug #2495 (only "might solve" because the bug does not come with a reproducible example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15461 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
known instances in unification.ml). This refines the fix to bug #1918. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-20Fixing bug #2809 (anomaly when printing a module with notations due toherbelin
bad interaction between lazy evaluation of pp streams and temporary effectful extension of global environment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15457 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-20Install compat5 module with grammar.cmapboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15456 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 13:25:47 +0000