diff options
Diffstat (limited to 'plugins/ltac/tacentries.ml')
| -rw-r--r-- | plugins/ltac/tacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index cd8c9e471..39121ac94 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -170,7 +170,7 @@ let add_tactic_entry (kn, ml, tg) state = TacGeneric arg in let l = List.map map l in - (TacAlias (loc,kn,l):raw_tactic_expr) + (TacAlias (loc,(kn,l)):raw_tactic_expr) in let () = if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then |