- fixed the Assert_failure error in kernel/modops

- fixed the problem with passing atomic tactics to ltacs
- restructured the distrib Makefile (can build a package from
  the CVS working dir)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 31 insertions, 13 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 25333b684..533919b67 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -230,11 +230,11 @@ let subst_constr_expr a loc subs =
   | COrderedCase (_,s,po,a,bl) ->
       COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl)
   | CLetTuple (_,nal,(na,po),a,b) ->
-      let na = name_app (subst_id subs) na in
+      let na = option_app (name_app (subst_id subs)) na in
       let nal = List.map (name_app (subst_id subs)) nal in
       CLetTuple (loc,nal,(na,option_app subst po),subst a,subst b)
   | CIf (_,c,(na,po),b1,b2) ->
-      let na = name_app (subst_id subs) na in
+      let na = option_app (name_app (subst_id subs)) na in
       CIf (loc,subst c,(na,option_app subst po),subst b1,subst b2)
   | CFix (_,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,subst t,subst d)) dl)
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 4cf3f25ab..101c29d31 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -275,10 +275,10 @@ GEXTEND Gram
     [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ]
   ;
   return_type:
-    [ [ a = OPT [ na = ["as"; id=name -> snd id | -> Names.Anonymous];
-              ty = case_type -> (na,ty) ] -> 
+    [ [ a = OPT [ na = OPT["as"; id=name -> snd id];
+                  ty = case_type -> (na,ty) ] -> 
         match a with 
-          | None -> Names.Anonymous, None
+          | None -> None, None
           | Some (na,t) -> (na, Some t)
     ] ]
   ;
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index b108ab4b4..4cdf0bc35 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -16,6 +16,8 @@ open Tacexpr
 open Rawterm
 open Genarg
 
+let compute = Cbv all_flags
+
 let tactic_kw =
   [ "->"; "<-" ]
 let _ = 
@@ -231,7 +233,7 @@ GEXTEND Gram
       | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
       | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
-      | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
+      | IDENT "compute" -> compute
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ SEP","-> Pattern pl ] ]
@@ -243,7 +245,7 @@ GEXTEND Gram
       | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
       | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
-      | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
+      | IDENT "compute" -> compute
       | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index dadfc18d0..2b3c17b14 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -159,11 +159,20 @@ let declare_tactic_v7 loc s cl =
       List.iter (Pptactic.declare_extra_tactic_pprule False $se$) $pp$;
     end
   >>
-(*
-let declare_atomic_extend s = 
-  Tacinterp.add_tacdef false
-    [(Names.id_of_string s,dummy_loc),Tacexpr.TacExtend(dummy_loc,s,[])]
-*)
+
+let rec contains_epsilon = function
+  | List0ArgType _ -> true
+  | List1ArgType t -> contains_epsilon t
+  | OptArgType _ -> true
+  | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2
+  | ExtraArgType("hintbases") -> true
+  | _ -> false
+let is_atomic =
+  List.for_all
+    (function
+        TacTerm _ -> false
+      | TacNonTerm(_,t,_,_) -> contains_epsilon t)
+
 let declare_tactic loc s cl =
   let (s',cl') = new_tac_ext (s,cl) in
   let pp' = make_printing_rule cl' in
@@ -184,12 +193,19 @@ let declare_tactic loc s cl =
   in
   let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in
   let se = mlexpr_of_string s in
+  let atomic_tactics =
+    mlexpr_of_list (fun (s,_,_) -> mlexpr_of_string s)
+      (List.filter (fun (_,al,_) -> is_atomic al) cl') in
   <:str_item<
     declare
       open Pcoq;
       declare $list:hidden$ end;
       try
-       Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ])
+        let _=Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ]) in
+        List.iter
+          (fun s -> Tacinterp.add_primitive_tactic s
+              (Tacexpr.TacAtom((0,0),Tacexpr.TacExtend((0,0),s,[]))))
+          $atomic_tactics$
       with e -> Pp.pp (Cerrors.explain_exn e);
       if Options.v7.val then Egrammar.extend_tactic_grammar $se'$ $gl$
       else Egrammar.extend_tactic_grammar $se'$ $gl'$;