diff options
Diffstat (limited to 'grammar/q_coqast.ml4')
| -rw-r--r-- | grammar/q_coqast.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index f59a4af32..25d4c0b23 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$, |