diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-08 03:22:22 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-07 02:55:41 +0200 |
commit | 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (patch) | |
tree | 24b4e369c4acbe2bb9c9ca79b84fc7ddff34e2d8 /grammar/tacextend.mlp | |
parent | fee2365f13900b4d4f4b88c986cbbf94403eeefa (diff) |
[camlpX] Remove camlp4 compat layer.
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.
Diffstat (limited to 'grammar/tacextend.mlp')
-rw-r--r-- | grammar/tacextend.mlp | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 8c0614a7b..f57be9022 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -10,7 +10,15 @@ open Q_util open Argextend -open GramCompat + +(** Quotation difference for match clauses *) + +let default_patt loc = + (<:patt< _ >>, Ploc.VaVal None, <:expr< failwith "Extension: cannot occur" >>) + +let make_fun loc cl = + let l = cl @ [default_patt loc] in + MLast.ExFun (loc, Ploc.VaVal l) (* correspond to <:expr< fun [ $list:l$ ] >> *) let dloc = <:expr< Loc.ghost >> @@ -41,11 +49,11 @@ let rec make_let raw e = function let make_clause (pt,_,e) = (make_patt pt, - vala None, + Ploc.VaVal None, make_let false e pt) let make_fun_clauses loc s l = - let map c = GramCompat.make_fun loc [make_clause c] in + let map c = make_fun loc [make_clause c] in mlexpr_of_list map l let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >> @@ -100,7 +108,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with whole-prof tactics like [shelve_unifiable]. *) <:expr< fun _ $lid:"ist"$ -> $tac$ >> | _ -> - let f = GramCompat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in + let f = make_fun loc [patt, Ploc.VaVal None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >> in (** Arguments are not passed directly to the ML tactic in the TacML node, @@ -129,7 +137,6 @@ let declare_tactic loc tacname ~level classification clause = match clause with ] open Pcaml -open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; |