Generate parsing rules for ML tactics in the same order as before a7917a32.

Once again showing the fragility of the parsing engine, commit a7917a32
reversed the relative order of the declaration of parsing rules for tactics
declared through TACTIC EXTEND. There is probably no good order at all, but
for retrocompatibility, this patch enforces the original one.

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)
 
 (**********************************************************************)