From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 parsing/tacextend.ml4 | 59 ++++++++++++++++++++++-----------------------------
 1 file changed, 25 insertions(+), 34 deletions(-)

(limited to 'parsing/tacextend.ml4')

diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 0d7a9cfe..2fe1fdda 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-
-(* $Id: tacextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
+(*i camlp4deps: "tools/compat5b.cmo" i*)
 
 open Util
 open Genarg
@@ -18,6 +16,7 @@ open Argextend
 open Pcoq
 open Extrawit
 open Egrammar
+open Compat
 
 let rec make_patt = function
   | [] -> <:patt< [] >>
@@ -43,20 +42,9 @@ let rec make_let e = function
       let loc = join_loc loc (MLast.loc_of_expr e) in
       let e = make_let e l in
       let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in
-      let v =
-        (* Special case for tactics which must be stored in algebraic
-           form to avoid marshalling closures and to be reprinted *)
-        if is_tactic_genarg t then
-          <:expr< ($v$, Tacinterp.eval_tactic $v$) >>
-        else v in
       <:expr< let $lid:p$ = $v$ in $e$ >>
   | _::l -> make_let e l
 
-let add_clause s (pt,e) l =
-  let p = make_patt pt in
-  let w = Some (make_when (MLast.loc_of_expr e) pt) in
-  (p, <:vala< w >>, make_let e pt)::l
-
 let rec extract_signature = function
   | [] -> []
   | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
@@ -69,12 +57,14 @@ let check_unicity s l =
       ("Two distinct rules of tactic entry "^s^" have the same\n"^
       "non-terminals in the same order: put them in distinct tactic entries")
 
-let make_clauses s l =
+let make_clause (pt,e) =
+  (make_patt pt,
+   vala (Some (make_when (MLast.loc_of_expr e) pt)),
+   make_let e pt)
+
+let make_fun_clauses loc s l =
   check_unicity s l;
-  let default =
-    (<:patt< _ >>,<:vala<None>>,
-     <:expr< failwith "Tactic extension: cannot occur" >>) in
-  List.fold_right (add_clause s) l [default]
+  Compat.make_fun loc (List.map make_clause l)
 
 let rec make_args = function
   | [] -> <:expr< [] >>
@@ -89,9 +79,7 @@ let rec make_eval_tactic e = function
       let p = Names.string_of_id p in
       let loc = join_loc loc (MLast.loc_of_expr e) in
       let e = make_eval_tactic e l in
-        (* Special case for tactics which must be stored in algebraic
-           form to avoid marshalling closures and to be reprinted *)
-      <:expr< let $lid:p$ = ($lid:p$,Tacinterp.eval_tactic $lid:p$) in $e$ >>
+      <:expr< let $lid:p$ = $lid:p$ in $e$ >>
   | _::l -> make_eval_tactic e l
 
 let rec make_fun e = function
@@ -165,30 +153,28 @@ let declare_tactic loc s cl =
   let atomic_tactics =
     mlexpr_of_list mlexpr_of_string
       (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in
-  <:str_item<
-    declare
-      open Pcoq;
-      open Extrawit;
-      declare $list:hidden$ end;
+  declare_str_items loc
+   (hidden @
+    [ <:str_item< do {
       try
-        let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in
+        let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in
         List.iter
           (fun s -> Tacinterp.add_primitive_tactic s
               (Tacexpr.TacAtom($default_loc$,
                  Tacexpr.TacExtend($default_loc$,s,[]))))
           $atomic_tactics$
-      with e -> Pp.pp (Cerrors.explain_exn e);
+      with e -> Pp.pp (Errors.print e);
       Egrammar.extend_tactic_grammar $se$ $gl$;
-      List.iter Pptactic.declare_extra_tactic_pprule $pp$;
-    end
-  >>
+      List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
+    ])
 
 open Pcaml
+open PcamlSig
 
 EXTEND
   GLOBAL: str_item;
   str_item:
-    [ [ "TACTIC"; "EXTEND"; s = [ UIDENT | LIDENT ];
+    [ [ "TACTIC"; "EXTEND"; s = tac_name;
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
          declare_tactic loc s l ] ]
@@ -214,5 +200,10 @@ EXTEND
         GramTerminal s
     ] ]
   ;
+  tac_name:
+    [ [ s = LIDENT -> s
+      | s = UIDENT -> s
+    ] ]
+  ;
   END
 
-- 
cgit v1.2.3