diff options
| author | Pierre-Marie Pédrot | 2013-09-06 21:50:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-11-27 18:43:35 +0100 |
| commit | 144f2ac7c7394a701808daa503a0b6ded5663fcc (patch) | |
| tree | c193b3e8ba6d2650213e8c0cc4f0c52f14eedba3 /grammar | |
| parent | 2923b9262e3859f2ad0169778d63d79843d7ddf7 (diff) | |
Adding generic solvers to term holes. For now, no resolution mechanism nor
parsing is plugged.
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 130f14717e..bfc38feb8b 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)) >> + | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),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 d0fd618c7f..02c00e3f0e 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -161,10 +161,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) -> + | Constrexpr.CHole (loc, None, None) -> let loc = of_coqloc loc in - <:expr< Constrexpr.CHole $dloc$ None >> - | Constrexpr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" + <:expr< Constrexpr.CHole $dloc$ None 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$, |