diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 52fa2a8607..cb67bb2ae5 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -285,7 +285,7 @@ open Evar_tactics (* evar creation *) TACTIC EXTEND evar - [ "evar" "(" ident(id) ":" constr(typ) ")" ] -> [ let_evar (Name id) typ ] + [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] END |