diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 694e88801c..0d4b479b44 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -175,7 +175,8 @@ END VERNAC COMMAND EXTEND AddSetoid [ "Add" "Setoid" constr(a) constr(aeq) constr(t) ] -> [ add_setoid a aeq t ] -| [ "Add" "Morphism" constr(m) ":" ident(s) ] -> [ new_named_morphism s m ] +| [ "Add" "Morphism" constr(m) ":" ident(s) ] -> + [ new_named_morphism s m None ] END VERNAC COMMAND EXTEND AddRelation1 |