| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-04-27 | Simplification in ppvernac.ml. | Hugo Herbelin | |
| 2016-04-27 | Removing unused generalization of pr_vernac over pr_constr and pr_lconstr. | Hugo Herbelin | |
| No other changes (long only because of a change of indentation). | |||
| 2016-04-27 | Fixing extra space in printing bullets. | Hugo Herbelin | |
| 2016-04-27 | Fixing space in printing <+ and <: + fixing missing Inline keyword. | Hugo Herbelin | |
| Fixing : in Declare Module. | |||
| 2016-04-27 | Fixing printing of Instance. | Hugo Herbelin | |
| 2016-04-27 | Fixing extra space in printing abbreviations (SyntaxDefinition). | Hugo Herbelin | |
| 2016-04-27 | Fixing printing of Polymorphic/Monomorphic. | Hugo Herbelin | |
| 2016-04-27 | Fixing printing of Arguments. | Hugo Herbelin | |
| 2016-04-27 | Printing notations as parsed. | Hugo Herbelin | |
| 2016-04-27 | Revert "Protect printing of intro-patterns from collision when "[|" or | Hugo Herbelin | |
| "|]"" because this commit triggers a Error: Files proofs/proofs.cma(Miscprint) and /usr/local/lib/ocaml/compiler-libs/ocamlcommon.cma(Lexer) make inconsistent assumptions over interface Lexer Adding two extra spaces systematically instead. This reverts commit 72be1f6beafafc3edd30df673fbb6c7e88f8fac7. | |||
| 2016-04-27 | Protect printing of ltac's "context [...]" from possible collision | Hugo Herbelin | |
| with user-level notations by inserting spaces. | |||
| 2016-04-27 | Protect printing of intro-patterns from collision when "[|" or "|]" | Hugo Herbelin | |
| exist as a keyword by inserting a space inbetween. | |||
| 2016-04-27 | Fixing printing of keeping hyp on the fly. | Hugo Herbelin | |
| 2016-04-27 | Fixing printing of inversion as. | Hugo Herbelin | |
| 2016-04-27 | Fixing extra space in printing destruct/induction as. | Hugo Herbelin | |
| 2016-04-27 | Fixing printing of induction/destruct as. | Hugo Herbelin | |
| 2016-04-27 | Fixing printing of pat%constr. | Hugo Herbelin | |
| 2016-04-27 | Honor parsing and printing levels for tactic entry in TACTIC EXTEND and | Hugo Herbelin | |
| VERNAC EXTEND. | |||
| 2016-04-27 | Temporary deactivate re-interpretation of terms in beautify. | Hugo Herbelin | |
| 2016-04-27 | In the short term, stronger invariant on the syntax of TacAssert, what | Hugo Herbelin | |
| allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause. | |||
| 2016-04-27 | So as to beautify to work, do not use notations in Inductive types | Hugo Herbelin | |
| with a clause where, nor Notation, nor Fixpoints. Should be certainly improved at least for Inductive types and Fixpoints, depending on whether there is a "where" clause for instance. | |||
| 2016-04-27 | A heuristic to add parentheses in the presence of rules such as | Hugo Herbelin | |
| Notation "## c" := (S c) (at level 0, c at level 100). which break the stratification of precedences. This works for the case of infix or suffix operators which occur in only one grammar rule, such as +, *, etc. This solves the "constr" part of #3709, even though this example is artificial. The fix is not complete. It puts extra parenthesese even when it is end of sentence, as in Notation "# c % d" := (c+d) (at level 3). Check fun x => # ## x % ## (x * 2). (* fun x : nat => # ## x % (## x * 2) *) The fix could be improved by not always using 100 for the printing level of "## c", but 100 only when not the end of the sentence. The fix does not solve the general problem with symbols occurring in more than one rule, as e.g. in: Notation "# c % d" := (c+d) (at level 1). Notation "## c" := (S c) (at level 0, c at level 5). Check fun x => # ## x % 0. (* Parentheses are necessary only if "0 % 0" is also parsable *) I don't see in this case what better approach to follow than restarting the parser to check reversibility of the printing. | |||
| 2016-04-27 | Attempt to slightly improve abusive "Collision between bound | Hugo Herbelin | |
| variables" when matching over "{v : _ | _ & _}" which hides twice the binding "fun v" since it is "sig2 (fun v => _) (fun v => _)". Computing the bound variables statically at internalisation time rather than every time at interpretation time. This cannot hurt even if I don't know how to deal with the "notation" problem of a single bound variable actually hiding two: at the current time, the notation is printed only if the two variables are identical (see #4592), so, with this semantics the warning should not be printed, but we lost the information that we are coming from a notation; if #4592 were addressed, then one of the binding should be alpha-renamed if they differ, so collision should be solved by choosing the variable name which is not renamed, but the matching algorithm should then be aware of what the notation printing algorithm is doing... maybe not the most critical thing at the current time. | |||
| 2016-04-25 | Removing dead code related to printing of ML tactics in Pptactic. | Pierre-Marie Pédrot | |
| 2016-04-19 | Revert "Fixing printing of surrounding parentheses in "ltac:"." | Hugo Herbelin | |
| I made a confusion between ltac: in constr and ltac: in tactics, the one needing parentheses in v8.5 but the latter needing parentheses only in trunk. This reverts commit f5dc54519f2a62bab2f7b9059e8c3c8dc53619be. | |||
| 2016-04-17 | Fixing printing of surrounding parentheses in "ltac:". | Hugo Herbelin | |
| 2016-04-14 | Moving and enhancing the grammar_tactic_prod_item_expr type. | Pierre-Marie Pédrot | |
| 2016-04-12 | Fixing printing of "destruct in" after ce71ac17268f. | Hugo Herbelin | |
| 2016-04-11 | Removing the ad-hoc tactic_expr type. | Pierre-Marie Pédrot | |
| This type was actually only used by the debug printer of tactics, and only for atomic tactics. Furthermore, that type was asymmetric, as the underlying tacexpr type was set to be glob_tactic, when the semantics would have required a Val.t type. Furthermore, this type is absent from every contrib I have seen, which hints again in favour of its lack of meaning. | |||
| 2016-04-10 | Extruding the print_atom primitive. | Pierre-Marie Pédrot | |
| 2016-04-09 | Removing extra spaces in printing arguments of VERNAC EXTEND. | Hugo Herbelin | |
| 2016-04-09 | Removing automatic printing of leading space in auto_using and | Hugo Herbelin | |
| hintbases so that it does not put extra space when auto is defined as a TACTIC EXTEND. | |||
| 2016-04-09 | Simplifying code for printing VERNAC EXTEND. | Hugo Herbelin | |
| 2016-04-09 | Fixing extra space in printing inductive types with no explicit type given. | Hugo Herbelin | |
| 2016-04-09 | In pr_clauses, do not print a leading space by default so that it can | Hugo Herbelin | |
| be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND. | |||
| 2016-04-08 | Fixing printing of toplevel values. | Pierre-Marie Pédrot | |
| This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all. | |||
| 2016-04-08 | Fixing printing of Tactic Notations with tactic arguments. | Pierre-Marie Pédrot | |
| 2016-04-04 | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵ | Matthieu Sozeau | |
| into JasonGross-trunk-function_scope | |||
| 2016-04-04 | Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into ↵ | Matthieu Sozeau | |
| aspiwack-linear-comparison Fixing a -1 -> +1 typo | |||
| 2016-03-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-25 | Univs: fix get_current_context (bug #4603, part I) | Matthieu Sozeau | |
| Return an evar_map with the right universes, when there are no focused subgoals or the proof is finished. | |||
| 2016-03-20 | Adding a new Ltac generic argument for forced tactics returing unit. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Refine to its proper module. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving the Ltac definition command to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Print Ltac to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tactic Notation to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing the untyped representation of genargs. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving VernacSolve to an EXTEND-based definition. | Pierre-Marie Pédrot | |
| 2016-03-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-13 | Supporting "(@foo) args" in patterns, where "@foo" has no arguments. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |