From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 parsing/q_coqast.ml4 | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'parsing/q_coqast.ml4')

diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 7df97a07..6e3b3f35 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -273,6 +273,11 @@ let mlexpr_of_message_token = function
   | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >>
   | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >>
 
+let mlexpr_of_debug = function
+  | Tacexpr.Off -> <:expr< Tacexpr.Off >>
+  | Tacexpr.Debug -> <:expr< Tacexpr.Debug >>
+  | Tacexpr.Info -> <:expr< Tacexpr.Info >>
+
 let rec mlexpr_of_atomic_tactic = function
   (* Basic tactics *)
   | Tacexpr.TacIntroPattern pl ->
@@ -399,15 +404,17 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
 
   (* Automation tactics *)
-  | Tacexpr.TacAuto (n,lems,l) ->
+  | Tacexpr.TacAuto (debug,n,lems,l) ->
+      let d = mlexpr_of_debug debug in
       let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
       let lems = mlexpr_of_list mlexpr_of_constr lems in
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
-      <:expr< Tacexpr.TacAuto $n$ $lems$ $l$ >>
-  | Tacexpr.TacTrivial (lems,l) ->
+      <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >>
+  | Tacexpr.TacTrivial (debug,lems,l) ->
+      let d = mlexpr_of_debug debug in
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
       let lems = mlexpr_of_list mlexpr_of_constr lems in
-      <:expr< Tacexpr.TacTrivial $lems$ $l$ >>
+      <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >>
 
   | _ -> failwith "Quotation of atomic tactic expressions: TODO"
 
-- 
cgit v1.2.3