diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_constr.ml4 | 4 | ||||
| -rw-r--r-- | grammar/q_coqast.ml4 | 7 |
2 files changed, 6 insertions, 5 deletions
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 index a731ade686..cf671adcb2 100644 --- a/grammar/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -18,7 +18,7 @@ let dloc = <:expr< Loc.ghost >> let apply_ref f l = <:expr< - Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$) + Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$, None), $mlexpr_of_list (fun x -> x) l$) >> EXTEND @@ -74,7 +74,7 @@ EXTEND | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] - | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$) >> + | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$, None) >> | c = match_constr -> c | "("; c = constr LEVEL "200"; ")" -> c ] ] ; diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index b3f60dee6a..9a0a22b9f1 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -140,10 +140,10 @@ let mlexpr_of_binder_kind = function $mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >> let rec mlexpr_of_constr = function - | Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (Id.to_string id) -> + | Constrexpr.CRef (Libnames.Ident (loc,id),_) when is_meta (Id.to_string id) -> let loc = of_coqloc loc in anti loc (Id.to_string id) - | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >> + | Constrexpr.CRef (r,n) -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ None >> | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" | Constrexpr.CProdN (loc,l,a) -> @@ -154,8 +154,9 @@ let rec mlexpr_of_constr = function let loc = of_coqloc loc in <:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> | Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CAppExpl (loc,a,l) -> + | Constrexpr.CAppExpl (loc,(p,r,us),l) -> let loc = of_coqloc loc in + let a = (p,r) in <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> | Constrexpr.CApp (loc,a,l) -> let loc = of_coqloc loc in |