aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
| | | | | | | | | | (the action is "clear"). Added subst_intropattern which was missing since the introduction of ApplyOn intro patterns. Still to do: make "intros _ ?id" working without interferences when "id" is precisely the internal name used for hypotheses to discard.
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
| | | | | | | | | | | so that one can retrieve them and pass them to third party tools (i.e. print the AST with the notations attached to the nodes concerned). Available syntax: - all in one: Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2"). - a posteriori: Format Notation "a /\ b" "latex" "#1 \wedge #2".
* Printing evar instance in a more intuitive order.Gravatar Hugo Herbelin2014-09-29
|
* Fix printing of primitive record info.Gravatar Matthieu Sozeau2014-09-29
|
* Print information about primitive records (Print and About).Gravatar Matthieu Sozeau2014-09-28
|
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-09-25
|
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
| | | | as a disjunctive intropattern.
* Fix a message.Gravatar Arnaud Spiwack2014-09-24
|
* coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".Gravatar Arnaud Spiwack2014-09-24
| | | This prevented the message from being silent when jumping ahead in a file. Fixes #3636.
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
| | | | | | | Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit.
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
| | | | | | | | contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
| | | | | | | | | | | | | of resulution for goals whose head is "ref". + means the argument is an input and shouldn't contain an evar, otherwise resolution fails. This generalizes the Typeclasses Strict Resolution option which prevents resolution to fire on underconstrained typeclass constraints, now the criterion can be applied to specific parameters. Also cleanup auto/eauto code, uncovering a potential backwards compatibility issue: in cases the goal contains existentials, we never use the discrimination net in auto/eauto. We should try to set this on once the contribs are stabilized (the stdlib goes through when the dnet is used in these cases).
* Not printing goal name (reinstalled by mistake in a previous commit).Gravatar Hugo Herbelin2014-09-15
|
* Fixing bug #3619 in emacs mode.Gravatar Hugo Herbelin2014-09-15
|
* Prepare goal name printing but no not print them at the current time.Gravatar Hugo Herbelin2014-09-13
|
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
| | | | in instances.
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
|
* Use evar name to print goal.Gravatar Hugo Herbelin2014-09-12
|
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
|
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
| | | | | instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
* Replace the list of argument in tacexpr with a single row argument.Gravatar Arnaud Spiwack2014-09-12
| | | | | | This has several benefits * It replicates the "no quadrillion-uple" pattern at the level of types. Giving names to the various component will hopefully make for better error messages. * It is less typo-prone, as the whole row can be passed as an argument rather than retyping each of the arguments. Also makes for a terser [Tacexpr]. * More importantly: local changes to tactic expressions will more often be kept local. Which will avoid some extra tedious work, and make rebases on top of such changes significantly easier.
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
|
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
| | | | | Left a README, just in case someone will discover the remnants of it decades from now.
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
|
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
|
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
|
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
|
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
| | | Dead code formerly used by the now defunct [autoinstances].
* Inductive and CoInductive records are printed correctly.Gravatar Arnaud Spiwack2014-09-04
|
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
| | | | Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
| | | | Just like the [Record] keyword allows only non-recursive records.
* Fixing printing of unreachable local tactics.Gravatar Pierre-Marie Pédrot2014-09-03
|
* Cleaning code in Pptactic.Gravatar Pierre-Marie Pédrot2014-09-02
| | | | | | Parametric printers are now using a record to ease the error reporting when modificating code. Further improvement may include the use of the object layer of OCaml, which would fit in this particular context.
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
|
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
|
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
| | | | | This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses don't respect Barendregt convention".
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
| | | | | | | | | | | now done entirely using declare_mind, which declares the associated constants for primitive records. This avoids a hack related to elimination schemes and ensures that the forward references to constants in the mutual inductive entry are properly declared just after the inductive. This also clarifies (and simplifies) the code of term_typing for constants which does not have to deal with building or checking projections anymore. Also fix printing of universes showing the de Bruijn encoding in a few places.
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
|
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
| | | | | Instead of having a version of unpackers for each level, we use a dummy argument to force unification of types.
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
|
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
|
* Space after [identity] coercion keywords (beautifier).Gravatar Xavier Clerc2014-08-21
|
* Avoid redundant spaces (beautifier).Gravatar Xavier Clerc2014-08-21
|
* Do not drop the locality qualifier (beautifier).Gravatar Xavier Clerc2014-08-21
|
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
| | | | | | | can be given with second H bound by the first one. Not very satisfied by passing closure to tactics.ml, but otherwise tactics would have to be aware of glob_constr.
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
| | | | | | | | | | | | | | | | - emphasizing the different kinds of patterns - factorizing code of the non-naming intro-patterns Still some questions: - Should -> and <- apply to hypotheses or not (currently they apply to hypotheses either when used in assert-style tactics or apply in, or when the term to rewrite is a variable, in which case "subst" is applied)? - Should "subst" be used when the -> or <- rewrites an equation x=t posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)? - Should -> and <- be applicable in non assert-style if the lemma has quantifications?
* Refine patch for behavior of unify_to_subterm to allow backtracking onGravatar Matthieu Sozeau2014-08-18
| | | | | | unsatisfiable constraint failures but give sensible error messages if an occurrence was found and only typeclass resolution failed. Fixes MathClasses.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 15:12:57 +0000