diff options
Diffstat (limited to 'ltac/tacentries.ml')
| -rw-r--r-- | ltac/tacentries.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 0be0dc7dc..2cc1b7b1c 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -357,16 +357,17 @@ let add_ml_tactic_notation name prods = Some id, GramNonTerminal (loc, etyp, e) in let prods = List.map (fun p -> List.map interp_prods p) prods in + let len = List.length prods in let iter i prods = let open Tacexpr in let (ids, prods) = List.split prods in let ids = List.map_filter (fun x -> x) ids in - let entry = { mltac_name = name; mltac_index = i } in + let entry = { mltac_name = name; mltac_index = len - i - 1 } in let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in let tac = TacML (Loc.ghost, entry, List.map map ids) in add_glob_tactic_notation false 0 prods true ids tac in - List.iteri iter prods; + List.iteri iter (List.rev prods); extend_atomic_tactic name (List.map (fun p -> List.map snd p) prods) (**********************************************************************) |