diff options
| author | Hugo Herbelin | 2014-09-30 09:13:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-30 09:30:53 +0200 |
| commit | 538b77dbb3b7799dc4d2e18033fc4fbf2eb26f7f (patch) | |
| tree | 53478ded9dfb8108402d7f45fa1300edd1569a20 /grammar | |
| parent | 2bbf1305a080667d8547c44b2684010aba3d8d45 (diff) | |
Add syntax for naming new goals in refine: writing ?[id] instead of _
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
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$, |