From 7f9203aa720dd16fa151d08d626124488c211994 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Apr 2003 08:35:20 +0000
Subject: Ajout cas Match

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3850 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/q_coqast.ml4 | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index dd1ce4ec26..54b928ef89 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -487,8 +487,11 @@ and mlexpr_of_tactic = function
       <:expr< Tacexpr.TacLetIn $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >>
 (*
   | Tacexpr.TacLetCut of (identifier * t * tactic_expr) list
-  | Tacexpr.TacMatch of t * (t * tactic_expr) list
 *)
+  | Tacexpr.TacMatch (t,l) ->
+      <:expr< Tacexpr.TacMatch
+        $mlexpr_of_may_eval mlexpr_of_constr t$
+        $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
   | Tacexpr.TacMatchContext (lr,l) ->
       <:expr< Tacexpr.TacMatchContext 
         $mlexpr_of_bool lr$
-- 
cgit v1.2.3