- 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

3 files changed, 21 insertions, 7 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index ac3f45577e..ae7b71c1c9 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -290,11 +290,11 @@ and ct_FORMULA =
   | CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST
   | CT_existvarc
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
-  | CT_if of ct_FORMULA * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
+  | CT_if of ct_FORMULA * ct_ID_OPT_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
   | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
   | CT_labelled_arg of ct_ID * ct_FORMULA
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
-  | CT_let_tuple of ct_ID_OPT_NE_LIST * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
+  | CT_let_tuple of ct_ID_OPT_NE_LIST * ct_ID_OPT_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
   | CT_letin of ct_DEF * ct_FORMULA
   | CT_notation of ct_STRING * ct_FORMULA_LIST
   | CT_num_encapsulator of ct_NUM_TYPE * ct_FORMULA
@@ -351,6 +351,10 @@ and ct_ID_OPT_NE_LIST =
 and ct_ID_OPT_OR_ALL =
     CT_coerce_ID_OPT_to_ID_OPT_OR_ALL of ct_ID_OPT
   | CT_all
+and ct_ID_OPT_OPT =
+    CT_coerce_ID_to_ID_OPT_OPT of ct_ID
+  | CT_coerce_ANONYMOUS_to_ID_OPT_OPT of ct_NONE
+  | CT_coerce_NONE_to_ID_OPT_OPT of ct_NONE
 and ct_ID_OR_INT =
     CT_coerce_ID_to_ID_OR_INT of ct_ID
   | CT_coerce_INT_to_ID_OR_INT of ct_INT
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 4c3288494e..d758113865 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -802,7 +802,7 @@ and fFORMULA = function
    fNODE "fixc" 2
 | CT_if(x1, x2, x3, x4, x5) ->
    fFORMULA x1;
-   fID_OPT x2;
+   fID_OPT_OPT x2;
    fFORMULA_OPT x3;
    fFORMULA x4;
    fFORMULA x5;
@@ -823,7 +823,7 @@ and fFORMULA = function
    fNODE "lambdac" 2
 | CT_let_tuple(x1, x2, x3, x4, x5) ->
    fID_OPT_NE_LIST x1;
-   fID_OPT x2;
+   fID_OPT_OPT x2;
    fFORMULA_OPT x3;
    fFORMULA x4;
    fFORMULA x5;
@@ -925,6 +925,12 @@ and fID_OPT_NE_LIST = function
    fID_OPT x;
    (List.iter fID_OPT l);
    fNODE "id_opt_ne_list" (1 + (List.length l))
+and fID_OPT_OPT = function
+| CT_coerce_ID_to_ID_OPT_OPT x -> fID x
+| CT_coerce_ANONYMOUS_to_ID_OPT_OPT x ->
+    fNONE x;
+    fNODE "anonymous" 1
+| CT_coerce_NONE_to_ID_OPT_OPT x -> fNONE x
 and fID_OPT_OR_ALL = function
 | CT_coerce_ID_OPT_to_ID_OPT_OR_ALL x -> fID_OPT x
 | CT_all -> fNODE "all" 0
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index cc06b43f3f..4ddcd21503 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -272,11 +272,15 @@ let rec xlate_match_pattern =
 ;;
 
 
+let xlate_id_opt_opt = function
+    Some (Name id) -> CT_coerce_ID_to_ID_OPT_OPT(CT_ident (string_of_id id))
+  | Some Anonymous -> CT_coerce_ANONYMOUS_to_ID_OPT_OPT CT_none
+  | None -> CT_coerce_NONE_to_ID_OPT_OPT CT_none
+
 let xlate_id_opt_aux = function
     Name id -> ctf_ID_OPT_SOME(CT_ident (string_of_id id))
   | Anonymous -> ctv_ID_OPT_NONE;;
 
-
 let xlate_id_opt (_, v) = xlate_id_opt_aux v;;
 
 let xlate_id_opt_ne_list = function
@@ -380,14 +384,14 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CLetTuple (_,a::l, (na,po), c, b) -> 
       CT_let_tuple(CT_id_opt_ne_list(xlate_id_opt_aux a,
 				     List.map xlate_id_opt_aux l),
-		   xlate_id_opt_aux na,
+		   xlate_id_opt_opt na,
 		   xlate_formula_opt po,
 		   xlate_formula c,
 		   xlate_formula b)
    | CLetTuple (_, [], _, _, _) -> xlate_error "NOT parsed: Let with ()"
    | CIf (_,c, (na, p), b1, b2) -> 
        CT_if
-	 (xlate_formula c, xlate_id_opt_aux na, xlate_formula_opt p,
+	 (xlate_formula c, xlate_id_opt_opt na, xlate_formula_opt p,
 	  xlate_formula b1, xlate_formula b2)
 
    | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->