aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
Commit message (Collapse)AuthorAge
* Merge PR #921: [make] remove compat5 file.Gravatar Maxime Dénès2017-08-01
|\
| * [make] remove compat5 file.Gravatar Emilio Jesus Gallego Arias2017-07-27
| | | | | | | | It is empty and not used anymore.
* | Removing default evar-normalization for ARGUMENT EXTEND.Gravatar Pierre-Marie Pédrot2017-07-26
|/ | | | This fixes bug 5650: evar (x : Prop) should not be slow.
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
| | | | | | | | | | | | This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge PR#759: don't leak unqualified identifiers from the macroGravatar Maxime Dénès2017-06-16
|\
| * don't leak unqualified identifiers from the macroGravatar Matej Košík2017-06-10
| |
* | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|/
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|
* Merge PR#698: Trunk miscGravatar Maxime Dénès2017-06-07
|\
* | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
* | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
| * make the expansion of the "DECLARE PLUGIN" closer to the way how a human ↵Gravatar Matej Kosik2017-05-30
|/ | | | would write that code
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
| |
| * Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| |
* | [location] Remove `Loc.internal_ghost`Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it.
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ | | | Now it is a private field, locations are optional.
* Fix compilation with camlp5 transitional mode.Gravatar Maxime Dénès2017-04-14
| | | | It was failing after 1d0eb5d4d6fea.
* [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.Gravatar Hugo Herbelin2017-03-22
| | | | This adds at least support for camlp5 6.14 (in addition to 6.17).
* Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-03-17
|\
| * TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-02-24
| | | | | | | | | | | | | | | | | | | | | | | | | | The syntax is: TACTIC EXTEND foo AT LEVEL i This commit makes it possible to define tacticals like the ssreflect arrow without having to resort to GEXTEND statements and intepretation hacks. Note that it simply makes accessible through the ML interface what Tactic Notation already supports: Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
* | [cleanup] Change Id.t option to Name.t in TacFunGravatar Tej Chajed2017-02-16
|/
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2016-11-03
|\
| * Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.Gravatar Pierre-Marie Pédrot2016-10-30
| |
* | Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-15
| |
* | Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
|/
* restore compatibility with gallium's camlp4 (broken by commit 8e07227c)Gravatar Pierre Letouzey2016-07-26
| | | | | | | | | | | | | | Apparently, in camlp4 (unlike camlp5) : - Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]" produces a kwd of type token instead of string (which sounds reasonable ?). For now, I've replaced kwd by the explicit strings. Not so nice, but works with both camlp4 and camlp5 - A quotation of the form "let obj = ... in bar; baz" is not interpreted in the usual OCaml way, but rather as "(let obj = ... in bar); baz". Let's use instead "let obj = ... in let () = bar in baz", which works fine.
* 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
* 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
* Makefile: compat5* moved in grammar/, less -I given to camlp4oGravatar Pierre Letouzey2016-06-21
|
* remove grammar/grammar.mllibGravatar Pierre Letouzey2016-06-08
| | | | | | grammar.cma is built by Makefile.build in a specific, hardcoded way. Let's remove this old .mllib file to avoid potential confusions in the future.
* Removing the Q_constr file.Gravatar Pierre-Marie Pédrot2016-06-05
|
* Merge branch 'yet-another-makefile-bigbang' into trunkGravatar Pierre Letouzey2016-06-01
|\
| * Yet another Makefile reform : a unique phase without nasty make tricksGravatar Pierre Letouzey2016-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We're back to a unique build phase (as before e372b72), but without relying on the awkward include-deps-failed-lets-retry feature of make. Since PMP has made grammar/ self-contained, we could now build grammar.cma in a rather straightforward way, no need for a specific sub-call to $(MAKE) for that. The dependencies between files of grammar/ are stated explicitely, since .d files aren't fully available initially. Some Makefile simplifications, for instance remove the CAMLP4DEPS shell horror. Instead, we generalize the use of two different filename extensions : - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule Note that we do not generate .ml4.d anymore (thanks to the .mlp vs. .ml4 dichotomy)
* | This patch splits pretty printing representation from IO operations.Gravatar Pierre-Marie Pédrot2016-05-31
|\ \ | |/ |/|
* | Making the grammar/ folder independent from the other ones.Gravatar Pierre-Marie Pédrot2016-05-31
| |
| * 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.
* Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments.Gravatar Pierre-Marie Pédrot2016-05-14
| | | | | | | | | | | | | | | | | | Since TACTIC EXTEND relies on the usual tactic notation mechanism, the interpretation of an ML tactic first goes through a TacAlias node. This means that variables bound by the notation overwrite those of the current environment. It turns out to be problematic for badly designed arguments that close over variables of the environment, e.g. glob_constr, because the variables used at interpretation time are now different from the ones of parsing time. Ideally, those arguments should return a closure made of the inner argument together with the Ltac environment they were defined in. Unluckily, this would need some important changes in their design. Most notably, most of ssreflect ARGUMENT EXTEND actually create such closed arguments. In order to emulate the old behaviour, we rather use a hack by prefixing ML-bound variables by a character that is not accessible from user-side.
* AlistNsep token now accepts an arbitrary separator.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
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
| |
* | Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
* | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | EXTEND and"" This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
* | Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
| | | | | | | | VERNAC EXTEND.