diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_constr.ml4 | 2 | ||||
| -rw-r--r-- | grammar/q_coqast.ml4 | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 index e1db0a05a3..bd3fac2e74 100644 --- a/grammar/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -70,7 +70,7 @@ EXTEND | "0" [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >> | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> - | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),None) >> + | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),Misctypes.IntroAnonymous,None) >> | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index f59a4af324..25d4c0b23c 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -166,10 +166,10 @@ let rec mlexpr_of_constr = function 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$ >> | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CHole (loc, None, None) -> + | Constrexpr.CHole (loc, None, ipat, None) -> let loc = of_coqloc loc in - <:expr< Constrexpr.CHole $dloc$ None None >> - | Constrexpr.CHole (loc, _, _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" + <:expr< Constrexpr.CHole $dloc$ None $mlexpr_of_intro_pattern_naming ipat$ None >> + | Constrexpr.CHole (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" | Constrexpr.CNotation(_,ntn,(subst,substl,[])) -> <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$ ($mlexpr_of_list mlexpr_of_constr subst$, |