aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Collapse)Author
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24correct some ends of .mllib files (avoid a broken tolink.ml)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15766 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15731 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-07Avoid Pp.std_ppcmds in Misctypes.sort_infoletouzey
Otherwise, after a Set Printing Universes we may end on a comparison of Pp.std_ppcmds, which may fail on functional values (cf. Constrextern.check_same_type), as notice by Pierre-Marie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15697 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-30Bigint: avoid dependency over Ppletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15664 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-21Slight modification to the printing of goals when in emacs mode.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15635 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-20Fixing test-suitepboutill
- bug in r15614: hnf was identity - fix Print Assumptions - bug in r15624: Dump glob of Print About only for Glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15630 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-19Getting rid of the undocumented [complete] tactic, which wasppedrot
redundant with [solve]. The AST node still exists in Ltac, because this is used by the [assert ... by ...] tactical. Fixes #2847. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15625 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-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-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-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-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-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-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-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-19Fixing some inconsistencies of constr printer wrt constr parserherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15447 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-14Internalization of pattern is done in two phases.pboutill
First Notations, syntactic definitions, primitive entries are tackled to build raw_cases_pattern_expr. Reference are revolved at this time too. Then raw_patterns are internalized as cases_pattern or applied inductive (dealing with implicit args, or_pattern refactoring, aliases). It is more uniform, it allows notations for non fully applied constructors but : - It does not raise a warning when an identifier is also a global_reference different than a constructor. - It looks for implicit arguments twice. (because finding scopes of arguments asks for implicit arguments). - It does not deal anymore with constants that evaluates to constructor. (This one is voluntary, dealing with implicit & notations is already a hell full of bugs so what will be next step ? Any terms that computes to a pattern ???) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15439 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-12Fixing test-suite after last storm in Pp.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-04Replacing some str with strbrkppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-30More uniformisation in Pp.warn functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29place all pretty-printing files in new dir printing/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 14:35:22 +0000