diff options
| author | Pierre-Marie Pédrot | 2014-09-09 22:13:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-10 00:16:20 +0200 |
| commit | edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 (patch) | |
| tree | e7af11e344a99b2496d22d2bc100f493bd701b96 /grammar | |
| parent | 0dd3f0d34873dcd126be8ec48724a310214f38ac (diff) | |
VernacExtend does not dispatch on type anymore.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/vernacextend.ml4 | 22 |
1 files changed, 8 insertions, 14 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 3a99916331..bda262a986 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -27,13 +27,6 @@ let rec make_let e = function <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> | _::l -> make_let e l -let check_unicity s l = - let l' = List.map (fun (_,l,_,_) -> extract_signature l) l in - if not (Util.List.distinct l') then - msg_warning - (strbrk ("Two distinct rules of entry "^s^" have the same "^ - "non-terminals in the same order: put them in distinct vernac entries")) - let make_clause (_,pt,_,e) = (make_patt pt, vala (Some (make_when (MLast.loc_of_expr e) pt)), @@ -83,11 +76,12 @@ let make_clause_classifier cg s (_,pt,c,_) = <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = - check_unicity s l; - Compat.make_fun loc (List.map make_clause l) + let cl = List.map (fun c -> Compat.make_fun loc [make_clause c]) l in + mlexpr_of_list (fun x -> x) cl let make_fun_classifiers loc s c l = - Compat.make_fun loc (List.map (make_clause_classifier c s) l) + let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in + mlexpr_of_list (fun x -> x) cl let mlexpr_of_clause = mlexpr_of_list @@ -101,15 +95,15 @@ let declare_command loc s c nt cl = let classl = make_fun_classifiers loc s c cl in declare_str_items loc [ <:str_item< do { - try do { - Vernacinterp.vinterp_add $se$ $funcl$; - Vernac_classifier.declare_vernac_classifier $se$ $classl$ } + try do { + CList.iteri (fun i f -> Vernacinterp.vinterp_add ($se$, i) f) $funcl$; + CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ } with [ e when Errors.noncritical e -> Pp.msg_warning (Pp.app (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) (Errors.print e)) ]; - Egramml.extend_vernac_command_grammar $se$ $nt$ $gl$ + CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; } >> ] open Pcaml |