Monomorphization (toplevel)

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

1 files changed, 9 insertions, 9 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 85abcc01ce..27f63d2f87 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -56,10 +56,9 @@ let typecheck_params_and_fields id t ps nots fs =
   let evars = ref Evd.empty in
   let _ = 
     let error bk (loc, name) = 
-      match bk with
-      | Default _ ->
-	  if name = Anonymous then 
-	    user_err_loc (loc, "record", str "Record parameters must be named")
+      match bk, name with
+      | Default _, Anonymous ->
+        user_err_loc (loc, "record", str "Record parameters must be named")
       | _ -> ()
     in
       List.iter 
@@ -153,7 +152,7 @@ let subst_projection fid l c =
   in
   let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *)
   let c'' = substrec 0 c' in
-  if !bad_projs <> [] then
+  if not (List.is_empty !bad_projs) then
     raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
   c''
 
@@ -222,7 +221,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
             with NotDefinable why ->
 	      warning_or_error coe indsp why;
 	      (None::sp_projs,NoProjection fi::subst) in
-      (nfi-1,(fi, optci=None)::kinds,sp_projs,subst))
+      (nfi-1,(fi, Option.is_empty optci)::kinds,sp_projs,subst))
       (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
@@ -266,7 +265,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
   let mie =
     { mind_entry_params = List.map degenerate_decl params;
       mind_entry_record = true;
-      mind_entry_finite = finite<>CoFinite;
+      mind_entry_finite = finite != CoFinite;
       mind_entry_inds = [mie_ind] } in
   let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
@@ -383,7 +382,8 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
     | _ -> acc in
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
   if not (List.distinct allnames) then error "Two objects have the same name";
-  if not (kind = Class false) && List.exists ((<>) None) priorities then
+  let isnot_class = match kind with Class false -> false | _ -> true in
+  if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     error "Priorities only allowed for type class substructures";
   (* Now, younger decl in params and fields is on top *)
   let sc = interp_and_check_sort s in
@@ -402,6 +402,6 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
 	let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs 
-	  fields is_coe (List.map (fun coe -> coe <> None) coers) sign in
+	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign;
 	IndRef ind