diff options
| author | herbelin | 2003-09-06 08:21:22 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-06 08:21:22 +0000 |
| commit | 3fa49ba9ee1a19f85ebe76f19700c8f747d628c3 (patch) | |
| tree | 7b9af34f114c82a1b5d963c81e2b25ef38810cb3 | |
| parent | e9c8f69be0e0158d493b45476246cb82f7eb5d5a (diff) | |
Passage de lconstr à constr pour les arguments immédiat de commandes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4313 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index ad78104cff..a32926bb19 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -113,11 +113,11 @@ GEXTEND Gram | IDENT "fail"; n = [ n = natural -> n | -> fail_default_value ]; s = [ s = STRING -> s | -> ""] -> TacFail (n,s) | st = simple_tactic -> TacAtom (loc,st) - | IDENT "eval"; rtc = red_expr; "in"; c = Constr.lconstr -> + | IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> TacArg(ConstrMayEval (ConstrEval (rtc,c))) | IDENT "inst"; id = identref; "["; c = Constr.lconstr; "]" -> TacArg(ConstrMayEval (ConstrContext (id,c))) - | IDENT "check"; c = Constr.lconstr -> + | IDENT "check"; c = Constr.constr -> TacArg(ConstrMayEval (ConstrTypeOf c)) | IDENT "fresh"; s = OPT STRING -> TacArg (TacFreshId s) |