- 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, 35 insertions, 34 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 60e6657d54..e28065afd8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1493,13 +1493,13 @@ let rec extern inctx scopes vars r =
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,nal,
-        (na,option_app (extern_type scopes (add_vname vars na)) typopt),
+        (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern false scopes (List.fold_left add_vname vars nal) b)
 
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
-        (na,option_app (extern_type scopes (add_vname vars na)) typopt),
+        (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars b1, sub_extern false scopes vars b2)
 
   | RRec (loc,fk,idv,tyv,bv) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index dfa6a1b94e..c6a819d440 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -757,13 +757,12 @@ let internalise sigma env allow_soapp lvar c =
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
     | CCases (loc, (po,rtnpo), tms, eqns) ->
-        let tms,rtnids = List.fold_right (fun (tm,indnalo) (inds,ids) ->
-          let tm' = intern env tm in
-	  let typ,ids = intern_return_type env indnalo tm' ids in
-	  (tm',ref typ)::inds,ids)
-	  tms ([],ids) in
-        let rtnpo =
-          option_app (intern_type (rtnids,tmp_scope,scopes)) rtnpo in
+        let tms,env' = List.fold_right
+          (fun citm (inds,env) ->
+	    let (tm,ind),nal = intern_case_item env citm in
+	    (tm,ref ind)::inds,List.fold_left (push_name_env lvar) env nal)
+	  tms ([],env) in
+        let rtnpo = option_app (intern_type env') rtnpo in
 	RCases (loc, (option_app (intern_type env) po, ref rtnpo), tms,
 		List.map (intern_eqn (List.length tms) env) eqns)
     | COrderedCase (loc, tag, po, c, cl) ->
@@ -773,15 +772,17 @@ let internalise sigma env allow_soapp lvar c =
 		  Array.of_list (List.map (intern env) cl),ref None)
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
-        RLetTuple (loc, nal,
-           (na, option_app (intern_type (push_name_env lvar env' na)) po),
-           intern env' b,
-	   intern (List.fold_left (push_name_env lvar) env nal) c)
+        let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
+        let env'' = List.fold_left (push_name_env lvar) env ids in
+        let p' = option_app (intern_type env'') po in
+        RLetTuple (loc, nal, (na', p'), b',
+                   intern (List.fold_left (push_name_env lvar) env nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
-	let env = reset_tmp_scope env in
-        RIf (loc, intern env c,
-           (na, option_app (intern_type (push_name_env lvar env na)) po),
-           intern env b1, intern env b2)
+	let env' = reset_tmp_scope env in
+        let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
+        let env'' = List.fold_left (push_name_env lvar) env ids in
+        let p' = option_app (intern_type env'') po in
+        RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole loc -> 
 	RHole (loc, QuestionMark)
     | CPatVar (loc, n) when allow_soapp ->
@@ -823,31 +824,31 @@ let internalise sigma env allow_soapp lvar c =
 	let env_ids = List.fold_right Idset.add eqn_ids ids in
 	(loc, eqn_ids,pl,intern (env_ids,tmp_scope,scopes) rhs)
 
-  and intern_return_type (vars,_,scopes as env) (na,t) tm ids =
+  and intern_case_item (vars,_,scopes as env) (tm,(na,t)) =
+    let tm' = intern env tm in
     let ids,typ = match t with
     | Some t -> 
 	let tids = names_of_cases_indtype t in
 	let tids = List.fold_right Idset.add tids Idset.empty in
 	let t = intern_type (tids,None,scopes) t in
 	begin match t with
-	  | RRef (loc,IndRef ind) -> ids,Some (loc,ind,[])
+	  | RRef (loc,IndRef ind) -> [],Some (loc,ind,[])
 	  | RApp (loc,RRef (_,IndRef ind),l) ->
 	      let nal = List.map (function
 		| RHole _ -> Anonymous
 		| RVar (_,id) -> Name id
 		| c ->
 		    user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
-	      List.fold_right (name_fold Idset.add) nal ids,
-	      Some (loc,ind,nal)
+	      nal, Some (loc,ind,nal)
 	  | _ -> error_bad_inductive_type (loc_of_rawconstr t)
 	end
     | None -> 
-	ids, None in
-    let na = match tm, na with
+	[], None in
+    let na = match tm', na with
       | RVar (_,id), None when Idset.mem id vars & not !Options.v7 -> Name id
       | _, None -> Anonymous
       | _, Some na -> na in
-    (na,typ), name_fold Idset.add na ids
+    (tm',(na,typ)), na::ids
 
   and iterate_prod loc2 env ty body = function
     | (loc1,na)::nal ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cc9488a3e3..7dda9a3175 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -347,9 +347,9 @@ type constr_expr =
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
-  | CLetTuple of loc * name list * (name * constr_expr option) *
+  | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
-  | CIf of loc * constr_expr * (name * constr_expr option)
+  | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of loc
   | CPatVar of loc * (bool * patvar)
@@ -510,13 +510,13 @@ let map_constr_expr_with_binders f g e = function
          List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | COrderedCase (loc,s,po,a,bl) ->
       COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl)
-  | CLetTuple (loc,nal,(na,po),b,c) ->
+  | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (name_fold g) nal e in
-      let e'' = name_fold g na e in
-      CLetTuple (loc,nal,(na,option_app (f e'') po),f e b,f e' c)
-  | CIf (loc,c,(na,po),b1,b2) ->
-      let e' = name_fold g na e in
-      CIf (loc,f e c,(na,option_app (f e') po),f e b1,f e b2)
+      let e'' = option_fold_right (name_fold g) ona e in
+      CLetTuple (loc,nal,(ona,option_app (f e'') po),f e b,f e' c)
+  | CIf (loc,c,(ona,po),b1,b2) ->
+      let e' = option_fold_right (name_fold g) ona e in
+      CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,f e t,f e d)) dl)
   | CCoFix (loc,id,dl) ->
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 65beaa511e..c6be360284 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -93,9 +93,9 @@ type constr_expr =
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
-  | CLetTuple of loc * name list * (name * constr_expr option) *
+  | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
-  | CIf of loc * constr_expr * (name * constr_expr option)
+  | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of loc
   | CPatVar of loc * (bool * patvar)