- 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

1 files changed, 12 insertions, 4 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 8fee8481d7..33eae08213 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