diff options
| author | Matthieu Sozeau | 2014-07-07 11:36:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-07 11:37:08 +0200 |
| commit | 200333fdc90a61665c04aca5fe58005e96738937 (patch) | |
| tree | 551b34e8dd4ee8bbcd3fd39225c044b2d47c440c | |
| parent | 20870c950ba3620755697010ffc49adb71cb4118 (diff) | |
Fix g_coqast for explicit applications.
| -rw-r--r-- | grammar/q_coqast.ml4 | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 528678d1d3..648407a707 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -125,6 +125,8 @@ let mlexpr_of_red_flags { Genredexpr.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$ } >> +let mlexpr_of_instance c = <:expr< None >> + let mlexpr_of_explicitation = function | Constrexpr.ExplByName id -> <:expr< Constrexpr.ExplByName $mlexpr_of_ident id$ >> | Constrexpr.ExplByPos (n,_id) -> <:expr< Constrexpr.ExplByPos $mlexpr_of_int n$ >> @@ -156,8 +158,8 @@ let rec mlexpr_of_constr = function | Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" | 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$ >> + let a = (p,r,us) in + <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_triple (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference mlexpr_of_instance a$ $mlexpr_of_list mlexpr_of_constr l$ >> | Constrexpr.CApp (loc,a,l) -> let loc = of_coqloc loc in <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >> |