aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
* Remove lexing of ordinal notations.Gravatar Maxime Dénès2016-07-03
| | | | | This was implemented in anticipation of a part of PR#164 that we decided not to merge.
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
|
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | Cf CHANGES for details.
* Parsing/compat.ml4: avoid "let open" syntax, unsupported by my camlp5 6.11Gravatar Pierre Letouzey2016-06-21
|
* Merge remote-tracking branch 'github/pr/212' into trunkGravatar Maxime Dénès2016-06-20
|\
| * Add file name, line number and beginning of line position to locations.Gravatar Maxime Dénès2016-06-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Coq locations already had support for this, but were containing dummy information. We now don't need anymore to reconstruct this information by browsing the file when printing an error message or enriching exceptions on the fly. It also became easier to interface with Coq since locations emitted by the lexer now always contain full information. On the API side, Loc.represent disappeared and Loc.t is now exposed as record. It is less error-prone than manipulating a tuple of 5 integers. Also, Loc.create takes 5 arguments instead of 3 and a pair.
* | Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq.
* | Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In pat%constr, creating new evars is now allowed only if "eintros" is given, i.e. "intros" checks that no evars are created, and similarly e.g. for "injection ... as ... pat%constr". The form "eintros [...]" or "eintros ->" with the case analysis or rewrite creating evars is now also supported. This is not a commitment to say that it is good to have an e- modifier to tactics. It is just to be consistent with the existing convention. It seems to me that the "no e-" variants are good for beginners. However, expert might prefer to use the e-variants by default. Opinions from teachers and users would be useful. To be possibly done: do that [= ...] work on hypotheses with side conditions or parameters based on the idea that they apply the full injection and not only the restriction of it to goals which are exactly an equality, as it is today.
| * Set required version of camlp5 to 6.06.Gravatar Maxime Dénès2016-06-17
|/ | | | | It is already very old (shipped with Debian oldstable) and adds file name support in locations.
* Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
| | | | | | | Suggested by R. Krebbers and C. Cohen, this makes modes more applicable, by allowing to trigger resolution on partially instantiated indices. This is a rough but fast approximation of the pattern on which one would like instances to apply.
* Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-06-16
|
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
| | | | | | simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
* Adding an only printing flag to notations.Gravatar Pierre-Marie Pédrot2016-06-07
|
* Removing the use to Egramcoq.recover_constr_grammar.Gravatar Pierre-Marie Pédrot2016-06-07
|
* Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
|
* Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
|
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | | | | | Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead.
* Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
|
* g_tactics : remove opt_bindings (2-line dead code)Gravatar Pierre Letouzey2016-06-01
|
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* The grammar_extend function now registers unsynchronized extensions.Gravatar Pierre-Marie Pédrot2016-05-11
| | | | | | This made little sense, as all the uses of this function were actually called from toplevel ML modules. This was at best useless, and at worst a source of bugs when loading plugins and messing with backtracking.
* Making the grammar command extend API purely functional.Gravatar Pierre-Marie Pédrot2016-05-11
| | | | | Instead of leaving the responsibility of extending the grammar to the caller, we ask for a list of extensions in the return value of the function.
* Moving the constr empty entry registering to the state-based API.Gravatar Pierre-Marie Pédrot2016-05-11
|
* Turning the grammar extend command API into a state-passing one.Gravatar Pierre-Marie Pédrot2016-05-11
|
* Moving the grammar summary to Pcoq.Gravatar Pierre-Marie Pédrot2016-05-11
|
* Delimiting the use of unsafe code in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Overlooked use of Gram instead of G module in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
| | | | This was probably wreaking havoc in tricky undo-redo scenarii.
* Further tidying of the constr extension code.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Type-safe constr notations.Gravatar Pierre-Marie Pédrot2016-05-10
| | | | | | | This removes the last call to unsafe_grammar_extend, so that all handwritten grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are still using the unsafe interface, but as they insert explicit casts they are deemed safe.
* AlistNsep token now accepts an arbitrary separator.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Simpler data structure for Arules token.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Purer implementation of empty level registering in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Hardening the obsolete unsafe_grammar_statement API.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Removing dead code in Compat.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
| |
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
| |
* | Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
* | Revert "Fixing a mispelling coma -> comma."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
* | Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
| |
* | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
* | Removing dead code in Compat.Gravatar Pierre-Marie Pédrot2016-04-25
| |
* | Remove dead registering code in Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * A fix to #4666 (Exc_located capsule added by camlp5 overwritingGravatar Hugo Herbelin2016-04-12
| | | | | | | | | | | | | | | | | | | | location set by lexer). This improves on abb4e7b0c by recovering the lexer location. AFAICS, it has an effect on lexer's errors Unterminated_comment and Unterminated_string. The other errors were not wrongly located, presumably because the Exc_located location added by camlp5 coincided with the location given by the lexer.
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2016-04-04
|\ \ | | | | | | | | | into JasonGross-trunk-function_scope
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 17:28:19 +0000