aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* This is an attempt to clarify terminology in choosing variable namesGravatar Hugo Herbelin2016-04-14
| | | | | | | | | in file indtypes.ml so that it is easier to follow what the code is doing. This is a purely alpha-renaming commit (if no mistakes). Note: was submitted as pull request #116.
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
|
* Uniformizing the semantics of ARGUMENT EXTEND macros.Gravatar Pierre-Marie Pédrot2016-04-13
|\ | | | | | | | | | | Most notably, we bring the single argument and three argument variants closer, so that the various TYPED AS clauses may be optional. Compile-time warnings have been added for redundant clauses.
| * Adding toplevel representation sharing for some generic arguments.Gravatar Pierre-Marie Pédrot2016-04-12
| |
| * Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
| |
| * Adding warnings for inferrable *_TYPED AS clauses.Gravatar Pierre-Marie Pédrot2016-04-12
| |
| * Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND.Gravatar Pierre-Marie Pédrot2016-04-12
| |
| * Warning for redundant TYPED AS clauses.Gravatar Pierre-Marie Pédrot2016-04-12
| |
| * Allowing simple ARGUMENT EXTEND not to mention their self type.Gravatar Pierre-Marie Pédrot2016-04-12
| | | | | | | | | | The TYPED AS clause was useless when defining a fresh generic argument. Instead of having to write it mandatorily, we simply make it optional.
| * Allowing the presence of TYPED AS in specialized ARGUMENT EXTEND.Gravatar Pierre-Marie Pédrot2016-04-12
|/ | | | | This allows to use the ARGUMENT EXTEND macro while sharing the same toplevel dynamic representation as another argument.
* Fixing printing of "destruct in" after ce71ac17268f.Gravatar Hugo Herbelin2016-04-12
|
* Removing the typed-level tactic_expr type.Gravatar Pierre-Marie Pédrot2016-04-11
|\
| * Removing the ad-hoc tactic_expr type.Gravatar Pierre-Marie Pédrot2016-04-11
| | | | | | | | | | | | | | | | | | | | 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.
| * Extruding the print_atom primitive.Gravatar Pierre-Marie Pédrot2016-04-10
|/
* Expliciting the fact that the atomic tactic type is self-contained.Gravatar Pierre-Marie Pédrot2016-04-10
|
* A small test of Print Ltac.Gravatar Hugo Herbelin2016-04-09
|
* Removing extra spaces in printing arguments of VERNAC EXTEND.Gravatar Hugo Herbelin2016-04-09
|
* Removing automatic printing of leading space in auto_using andGravatar Hugo Herbelin2016-04-09
| | | | | hintbases so that it does not put extra space when auto is defined as a TACTIC EXTEND.
* Re-add printer for tacdef_body so that Ltac definitions are printed by ↵Gravatar Hugo Herbelin2016-04-09
| | | | pr_vernac.
* Simplifying code for printing VERNAC EXTEND.Gravatar Hugo Herbelin2016-04-09
|
* Fixing extra space in printing inductive types with no explicit type given.Gravatar Hugo Herbelin2016-04-09
|
* In pr_clauses, do not print a leading space by default so that it canGravatar Hugo Herbelin2016-04-09
| | | | | | | be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\
| * Added compatibility coercions from Specif.v which were present in Coq 8.4.Gravatar Hugo Herbelin2016-04-08
| |
| * Fixing a source of inefficiency and an artificial dependency in theGravatar Daniel de Rauglaudre2016-04-08
| | | | | | | | | | | | | | printer in the congruence tactic. Debugging messages were always built even when not in the verbose mode of congruence.
* | Fixing printing of toplevel values.Gravatar Pierre-Marie Pédrot2016-04-08
| | | | | | | | | | | | | | 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.
* | Fixing printing of Tactic Notations with tactic arguments.Gravatar Pierre-Marie Pédrot2016-04-08
| |
| * Allow to unset the refinement mode of Instance in MLGravatar Matthieu Sozeau2016-04-07
| | | | | | | | | | | | Falling back to the global setting if not given. Useful to make Add Morphism fail correctly when the given proof terms are incomplete. Adapt test-suite file #2848 accordingly.
| * Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-04-07
| | | | | | | | | | | | product in setoid_rewrite. Backport of d670c6b6ce from trunk.
| * Merge PR#152: Add -compat 8.4 econstructor tactics, and testsGravatar Maxime Dénès2016-04-07
| |\
* | | An example which failed in 8.5 and that d670c6b6 fixes.Gravatar Hugo Herbelin2016-04-07
| | | | | | | | | | | | Thanks to Matthieu for the example.
| * | Use -win32 and -win64 suffixes for installer name on Windows.Gravatar Maxime Dénès2016-04-07
| | |
| | * Add -compat 8.4 econstructor tactics, and testsGravatar Jason Gross2016-04-05
| |/ | | | | | | | | Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in 8.4.
| * Fix bug #4656Gravatar Jason Gross2016-04-05
| | | | | | | | | | I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd; Coq.Init.Notations.constructor does not take any arguments.
| * Update Coq84.vGravatar Jason Gross2016-04-04
| | | | | | | | We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit.
| * Add compatibility Nonrecursive Elimination SchemesGravatar Jason Gross2016-04-04
| |
* | Fix after merge, the revert of Bind Scope applies to trunk only.Gravatar Matthieu Sozeau2016-04-04
| |
* | Merge remote-tracking branch 'origin/pr/78' into trunk:Gravatar Maxime Dénès2016-04-04
|\ \ | | | | | | | | | | | | An .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output.
* \ \ Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunkGravatar Matej Kosik2016-04-04
|\ \ \
* \ \ \ Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive ↵Gravatar Matej Kosik2016-04-04
|\ \ \ \ | | | | | | | | | | | | | | | defs in Print Assumptions"
| | * \ \ Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2016-04-04
| | |\ \ \ | | | | | | | | | | | | | | | | | | into JasonGross-trunk-function_scope
| | * | | | Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into ↵Gravatar Matthieu Sozeau2016-04-04
| |/| | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | aspiwack-linear-comparison Fixing a -1 -> +1 typo
| | | | | * Fixing the "No applicable tactic" non informative error messageGravatar Hugo Herbelin2016-04-03
| | | | | | | | | | | | | | | | | | | | | | | | regression on apply.
* | | | | | Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations.
* | | | | | Providing an API to access the parsing engine summary in a first-class way.Gravatar Pierre-Marie Pédrot2016-03-31
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of hardwiring a few special cases in Egramcoq, we allow the grammar state to contain arbitrary data structures. This permits to extend the parsing engine while retaining the synchronization with the global state, e.g. for use in plugins.
| * | | | | | Adding a test for bug #1850.Gravatar Pierre-Marie Pédrot2016-03-31
| | | | | | |
| * | | | | | Moving the code handling tactic notations to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
| | | | | | |
| * | | | | | Abstracting away the Summary-synchronized grammar-modifying commands.Gravatar Pierre-Marie Pédrot2016-03-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We provide an API so that external code such as plugins can define grammar extensions synchronized with the summary. This API is not perfect yet and is a mere abstraction of the current behaviour. In particular, it expects the user to modify the parser in an imperative way.
| * | | | | | Moving the Tactic Notation entry parser from Pcoq to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
|/ / / / / /
* | | | | | Ensuring that the type of base generic arguments contain triples.Gravatar Pierre-Marie Pédrot2016-03-30
| | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 05:52:50 +0000