- 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, 14 insertions, 7 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 8fee8481d..33eae0821 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -115,9 +115,11 @@ and merge_with env mtb with_decl =
 		let _ = subst_modtype (map_msid msid (MPself msid)) mtb in
 		  ()
 	      with
-		  Assert_failure _ -> error_circular_with_module id
+		  Failure _ -> error_circular_with_module id
 	    end;
-	    let cst = check_subtypes env' mtb old.msb_modtype in
+	    let cst =
+              try check_subtypes env' mtb old.msb_modtype
+              with Failure _ -> error_with_incorrect (label_of_id id) in
 	    let equiv = 
  	      match old.msb_equiv with
 		| None -> Some mp
@@ -213,7 +215,10 @@ and translate_module env is_definition me =
 	    | None -> mtb1, None, Constraint.empty
 	    | Some mte -> 
 		let mtb2 = translate_modtype env mte in
-		  mtb2, Some mtb2, check_subtypes env mtb1 mtb2
+                let cst =
+                  try check_subtypes env mtb1 mtb2
+                  with Failure _ -> error "not subtype" in
+		mtb2, Some mtb2, cst
 	in
 	  { mod_type = mtb;
 	    mod_user_type = mod_user_type;
@@ -237,7 +242,10 @@ and translate_mexpr env mexpr = match mexpr with
       let ftb = scrape_modtype env ftb in
       let farg_id, farg_b, fbody_b = destr_functor ftb in
       let meb,mtb = translate_mexpr env mexpr in
-      let cst = check_subtypes env mtb farg_b in
+      let cst =
+        try check_subtypes env mtb farg_b
+        with Failure _ ->
+          error "" in
       let mp = 
 	try
 	  path_of_mexpr mexpr 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 7459dcad8..569580bfb 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -125,12 +125,12 @@ let rec check_modpath_equiv env mp1 mp2 =
 let rec subst_modtype sub = function
   | MTBident ln -> MTBident (subst_kn sub ln)
   | MTBfunsig (arg_id, arg_b, body_b) ->
-      assert (not (occur_mbid arg_id sub));
+      if occur_mbid arg_id sub then failwith "capture";
       MTBfunsig (arg_id, 
 		 subst_modtype sub arg_b, 
 		 subst_modtype sub body_b)
   | MTBsig (sid1, msb) -> 
-      assert (not (occur_msid sid1 sub));
+      if occur_msid sid1 sub then failwith "capture";
       MTBsig (sid1, subst_signature sub msb)
 
 and subst_signature sub sign = 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6b0931a9e..50aeaf347 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -244,4 +244,3 @@ and check_modtypes cst env mtb1 mtb2 equiv =
 	  
 let check_subtypes env sup super = 
   check_modtypes Constraint.empty env sup super false
-