diff options
| author | herbelin | 2003-04-07 08:35:20 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-07 08:35:20 +0000 |
| commit | 7f9203aa720dd16fa151d08d626124488c211994 (patch) | |
| tree | 076d4e139d99a4e356b92f88e3d8986815d26903 | |
| parent | c9d2695b54adce95856f781cd6a6a1f085dafd5f (diff) | |
Ajout cas Match
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3850 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/q_coqast.ml4 | 5 |
1 files changed, 4 insertions, 1 deletions
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$ |