From f848b8bf579ed8fa7613174388a8fbc9ab2f6344 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 17 Mar 2009 20:14:19 +0000
Subject: - gros commit sur ring et field: passage des arguments simplifie -
 tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient   pas
 evalues, laissant des variables libres (symptome: exc Not_found) - reals:
 Open Local --> Local Open - ListTactics: syntaxe des listes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11989 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9df3ba4ec0..4102fae16a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2057,7 +2057,8 @@ and interp_genarg ist gl x =
       match tactic_genarg_level s with
       | Some n -> 
           (* Special treatment of tactic arguments *)
-          in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
+          in_gen (wit_tactic n)
+	    (TacArg(valueIn(val_interp ist gl (out_gen (globwit_tactic n) x))))
       | None -> 
           lookup_interp_genarg s ist gl x
 
@@ -2834,20 +2835,11 @@ let make_absolute_name ident repl =
     user_err_loc (loc,"Tacinterp.add_tacdef",
 		 str "There is no Ltac named " ++ pr_reference ident ++ str".")
 
-let rec filter_map f l = 
-  let rec aux acc = function
-      [] -> acc
-    | hd :: tl -> 
-	match f hd with
-	    Some x -> aux (x :: acc) tl
-	  | None -> aux acc tl
-  in aux [] l
-      
 let add_tacdef isrec tacl =
   let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
   let ist =
     {(make_empty_glob_sign()) with ltacrecvars = 
-	if isrec then filter_map 
+	if isrec then list_map_filter
 	  (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun 
 	else []} in
   let gtacl =
-- 
cgit v1.2.3