From 9462ef0ad6eb233c2f74bb400a262ddefd880386 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 May 2016 11:17:45 +0200 Subject: 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. --- ltac/tacentries.ml | 5 +++-- 1 file 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) (**********************************************************************) -- cgit v1.2.3