Fix bug #1936: uncaught exception due to undefinable exceptions.

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

1 files changed, 44 insertions, 43 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index c7ba7fa44..f63ae3ecb 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -201,47 +201,47 @@ let new_class id par ar sup props =
     let params = ctx_params and fields = ctx_props in
       List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
       match fields with
-	  [(Name proj_name, _, field)] ->
-	    let class_body = it_mkLambda_or_LetIn field params in
-	    let class_type = 
-	      match ar with
-		  Some _ -> Some (it_mkProd_or_LetIn arity params)
-		| None -> None
-	    in
-	    let class_entry = 
-	      { const_entry_body = class_body;
-		const_entry_type = class_type;
-		const_entry_opaque = false;
-		const_entry_boxed = false }
-	    in
-	    let cst = Declare.declare_constant (snd id)
-	      (DefinitionEntry class_entry, IsDefinition Definition) 
-	    in
-	    let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in
-	    let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
-	    let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
-	    let proj_entry = 
-	      { const_entry_body = proj_body;
-		const_entry_type = Some proj_type;
-		const_entry_opaque = false;
-		const_entry_boxed = false }
-	    in
-	    let proj_cst = Declare.declare_constant proj_name
-	      (DefinitionEntry proj_entry, IsDefinition Definition) 
-	    in
-	    let cref = ConstRef cst in
-	      Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps;
-	      Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls);
-	      set_rigid cst;
-	      cref, [proj_name, proj_cst]
-	| _ ->
-	    let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
-	    let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
-	    let kn = Record.declare_structure (snd id) idb arity_imps
-	      params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
-	    in
-	      IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
-				 (List.rev fields) (Recordops.lookup_projections (kn,0)))
+      | [(Name proj_name, _, field)] ->
+	  let class_body = it_mkLambda_or_LetIn field params in
+	  let class_type = 
+	    match ar with
+	    | Some _ -> Some (it_mkProd_or_LetIn arity params)
+	    | None -> None
+	  in
+	  let class_entry = 
+	    { const_entry_body = class_body;
+	      const_entry_type = class_type;
+	      const_entry_opaque = false;
+	      const_entry_boxed = false }
+	  in
+	  let cst = Declare.declare_constant (snd id)
+	    (DefinitionEntry class_entry, IsDefinition Definition) 
+	  in
+	  let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in
+	  let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
+	  let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
+	  let proj_entry = 
+	    { const_entry_body = proj_body;
+	      const_entry_type = Some proj_type;
+	      const_entry_opaque = false;
+	      const_entry_boxed = false }
+	  in
+	  let proj_cst = Declare.declare_constant proj_name
+	    (DefinitionEntry proj_entry, IsDefinition Definition) 
+	  in
+	  let cref = ConstRef cst in
+	    Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps;
+	    Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls);
+	    set_rigid cst;
+	    cref, [proj_name, Some proj_cst]
+      | _ ->
+	  let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
+	  let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
+	  let kn = Record.declare_structure (snd id) idb arity_imps
+	    params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
+	  in
+	    IndRef (kn,0), (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
+			       (List.rev fields) (Recordops.lookup_projections (kn,0)))
   in
   let ctx_context =
     List.map (fun ((na, b, t) as d) -> 
@@ -256,7 +256,8 @@ let new_class id par ar sup props =
       cl_props = ctx_props;
       cl_projs = projs }
   in
-    List.iter2 (fun p sub -> if sub then declare_instance_cst true (snd p))
+    List.iter2 (fun p sub -> 
+      if sub then match snd p with Some p -> declare_instance_cst true p | None -> ())
       k.cl_projs subs;
     add_class k
     
@@ -429,7 +430,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 		  try 
 		    let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
 		    let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
-		      Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
+		      Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
 		      c :: props, rest'
 		  with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
 		([], props) k.cl_props