aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/q_coqast.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/q_coqast.ml4')
-rw-r--r--grammar/q_coqast.ml46
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$,