summaryrefslogtreecommitdiff
path: root/parsing/q_coqast.ml4
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /parsing/q_coqast.ml4
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'parsing/q_coqast.ml4')
-rw-r--r--parsing/q_coqast.ml48
1 files changed, 6 insertions, 2 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index b5b07091..23d24497 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: q_coqast.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
+(* $Id: q_coqast.ml4 9315 2006-10-29 21:53:30Z barras $ *)
open Util
open Names
@@ -441,8 +441,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
$mlexpr_of_bool lz$
$mlexpr_of_bool lr$
$mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
+
+ | Tacexpr.TacFun (idol,body) ->
+ <:expr< Tacexpr.TacFun
+ ($mlexpr_of_list mlexpr_of_ident_option idol$,
+ $mlexpr_of_tactic body$) >>
(*
- | Tacexpr.TacFun of $dloc$ * tactic_fun_ast
| Tacexpr.TacFunRec of $dloc$ * identifier * tactic_fun_ast
*)
(*