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

5 files changed, 58 insertions, 53 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index b2489eac19..e966c3afc7 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -166,7 +166,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	    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
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 29655841f5..783bb50fd5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -41,7 +41,7 @@ type typeclass = {
   cl_props : rel_context;
   
   (* The method implementaions as projections. *)
-  cl_projs : (identifier * constant) list;
+  cl_projs : (identifier * constant option) list;
 }
 
 type typeclasses = (global_reference, typeclass) Gmap.t
@@ -148,7 +148,7 @@ let subst (_,subst,(cl,m,inst)) =
       (na, Option.smartmap do_subst b, do_subst t)))
       ctx
   in
-  let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, do_subst_con y)) projs in
+  let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, Option.smartmap do_subst_con y)) projs in
   let subst_class k cl classes = 
     let k = do_subst_gr k in
     let cl' = { cl_impl = k;
@@ -177,8 +177,8 @@ let discharge (_,(cl,m,inst)) =
     let ctx, _ =
       List.fold_right
 	(fun (gr, (id, b, t)) (ctx, k) -> 
-	  let gr' = Option.map (fun (gr, b) -> Lib.discharge_global gr, b) gr in
-	    ((gr', (id, Option.map (substn_vars k subst) b, substn_vars k subst t)) :: ctx), succ k)
+	  let gr' = Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b) gr in
+	    ((gr', (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t)) :: ctx), succ k)
 	rel ([], 0)
     in ctx
   in
@@ -198,7 +198,7 @@ let discharge (_,(cl,m,inst)) =
 	  cl_context = 
 	    List.map (fun (na,impl,b,t) -> None, (Name na,b,t)) ctx @
 	      (discharge_context (List.map (fun (na, _, _, _) -> na) ctx) cl.cl_context);
-	  cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs }
+	  cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs }
     in Gmap.add cl_impl' cl' acc
   in
   let classes = Gmap.fold subst_class cl Gmap.empty in
@@ -246,7 +246,10 @@ let update () =
 
 let add_class c = 
   classes := Gmap.add c.cl_impl c !classes;
-  methods := List.fold_left (fun acc x -> Gmap.add (snd x) c.cl_impl acc) !methods c.cl_projs;
+  methods := List.fold_left (fun acc x -> 
+    match snd x with
+    | Some m -> Gmap.add m c.cl_impl acc
+    | None -> acc) !methods c.cl_projs;
   update ()
     
 let class_info c = 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a9f91dc6f8..706f116563 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -35,8 +35,9 @@ type typeclass = {
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : rel_context;
 
-  (* The methods implementations of the typeclass as projections. *)
-  cl_projs : (identifier * constant) list;
+  (* The methods implementations of the typeclass as projections. Some may be undefinable due to 
+     sorting restrictions. *)
+  cl_projs : (identifier * constant option) list;
 }
 
 type instance
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 2d4f6715e7..70252f2b78 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -539,7 +539,7 @@ let morphism_class =
 let morphism_proxy_class = 
   lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.MorphismProxy"))))
 
-let respect_proj = lazy (mkConst (snd (List.hd (Lazy.force morphism_class).cl_projs)))
+let respect_proj = lazy (mkConst (Option.get (snd (List.hd (Lazy.force morphism_class).cl_projs))))
 
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index c7ba7fa44a..f63ae3ecbe 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