aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
Commit message (Collapse)AuthorAge
* Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Gravatar Pierre-Marie Pédrot2018-06-29
| | | | | | | | | The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one.
* Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
| | | | | | | | | Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
| | | | | | | | | | | | | | In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code.
* Remove syntax for classification in TACTIC EXTEND.Gravatar Maxime Dénès2017-12-22
| | | | It was left ignored after 8089dc960c9e8caf778907fd87be48d77b066433.
* [stm] Remove all but one use of VtUnknown.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | | | | | Together with #1122, this makes `VernacInstance` the only command in the Coq codebase that cannot be statically determined to open a proof. The reasoning for the commands moved to `VtSideff` is that parser-altering commands should be always marked `VtNow`; the rest can be usually marked as `VtLater`.
* Fix deprecated syntax warning from vernacextend.mlp.Gravatar Gaëtan Gilbert2017-11-24
|
* [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it.
* [plugin] Encapsulate modifiers to vernac commands.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | This is a continuation on #6183 and another step towards a more functional interpretation of commands. In particular, this should allow us to remove the locality hack.
* [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| | | | | | | | To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state.
* Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵Gravatar Maxime Dénès2017-11-06
|\ | | | | | | rules
* | Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
| |
* | Improving checks about the list separator in tactic notations.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | In Tactic Notation and TACTIC EXTEND, when an argument not ending with "_list_sep" was given with a separator, the separator was silently ignored. Now: - we take it into account if it is a list (i.e. ending with "_list"), as if "_list_sep" was given, since after all, the "_sep" is useless in the name. - we fail if there is a separator but it is not a "_list" or "_list_sep".
| * provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesGravatar Matej Košík2017-11-01
|/ | | | | | | | | | | | | | | Originally, it was not possible to define a new vernacular command in the following way: VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY [ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ] END because "loc : Loc.t" was not bound. This commit fixes that, i.e. the location of the custom Vernacular command (within *.v file) is made available as "loc" variable bound on the right side of "->" .
* 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)