From 76ed85857b467d38200a75b3dc7cd02d2d48b063 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 15 May 2002 20:13:06 +0000
Subject: Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de
 gauche à droite des hypothèses dans Intuition

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2696 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacinterp.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index e3d2a36702..b9a1f23a78 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -761,6 +761,9 @@ and letcut_interp ist ast = function
 
 (* Interprets the Match Context expressions *)
 and match_context_interp ist ast lmr g =
+  let lr,lmr = match lmr with 
+    | Str(_,dir)::lmr ->  (dir="LR",lmr)
+    | _ -> anomaly "Ill-formed Match Context" in
 (*  let goal =
     (match goalopt with
     | None ->
@@ -795,8 +798,9 @@ and match_context_interp ist ast lmr g =
        with No_match | _ ->
          apply_match_context ist goal tl)
     | (Pat (mhyps,mgoal,mt))::tl ->
-      let hyps = make_hyps (pf_hyps goal)
-      and concl = pf_concl goal in
+      let hyps = make_hyps (pf_hyps goal) in
+      let hyps = if lr then List.rev hyps else hyps in
+      let concl = pf_concl goal in
       (match mgoal with
       |	Term mg ->
         (try
-- 
cgit v1.2.3