Que des niveaux d'univers frais dans le type des constantes globales

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

4 files changed, 106 insertions, 112 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 1962318f9..962d26911 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -85,6 +85,7 @@ let coq_fleche = lazy(constant ["Setoid"] "fleche")
 let coqeq = lazy(global_constant ["Logic"] "eqT")
 
 let coqconj = lazy(global_constant ["Logic"] "conj")
+let coqand = lazy(global_constant ["Logic"] "and")
 
 (************************* Table of declared setoids **********************)
 
@@ -210,53 +211,62 @@ let find_theory a =
     
 (* Add a Setoid to the database after a type verification. *)
 
+let eq_lem_common_sign env a eq =
+  let na = named_hd env a Anonymous in
+  let ne = named_hd env eq Anonymous in
+  [(ne,None,mkApp (eq, [|(mkRel 3);(mkRel 2)|]));
+   (ne,None,mkApp (eq, [|(mkRel 4);(mkRel 3)|]));
+   (na,None,a);(na,None,a);(na,None,a);(na,None,a)]
+
 (* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->(eq a c)->(eq b d) *)
 let eq_lem_proof env a eq sym trans = 
-  lambda_create env
-    (a, lambda_create env
-       (a, lambda_create env
-	  (a, lambda_create env 
-	     (a, lambda_create env 
-		((mkApp (eq, [|(mkRel 4);(mkRel 3)|])), lambda_create env
-		   ((mkApp (eq, [|(mkRel 3);(mkRel 2)|])), lambda_create env
-		      ((mkApp (eq, [|(mkRel 6);(mkRel 4)|])),
-		       (mkApp (trans,
-			       [|(mkRel 6);(mkRel 7);(mkRel 4);
-				 (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|]));
-				 (mkApp (trans,
-					 [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|]
-			      )))))))))
+  let sign = eq_lem_common_sign env a eq in
+  let ne = named_hd env eq Anonymous in
+  let sign = (ne,None,mkApp (eq, [|(mkRel 6);(mkRel 4)|]))::sign in
+  let ccl = mkApp (eq, [|(mkRel 6);(mkRel 4)|]) in
+  let body =
+    mkApp (trans,
+      [|(mkRel 6);(mkRel 7);(mkRel 4);
+        (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|]));
+	  (mkApp (trans,
+	    [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|]) in
+  let p = it_mkLambda_or_LetIn body sign in
+  let t = it_mkProd_or_LetIn ccl sign in
+  (p,t)
 
 (* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->((eq a c)<->(eq b d)) *)
-let eq_lem2_proof env a eq sym trans = 
-  lambda_create env
-    (a, lambda_create env
-       (a, lambda_create env
-	  (a, lambda_create env 
-	     (a, lambda_create env 
-		((mkApp (eq, [|(mkRel 4);(mkRel 3)|])), lambda_create env
-		   ((mkApp (eq, [|(mkRel 3);(mkRel 2)|])),
-		    (mkApp ((Lazy.force coqconj),
-			    [|(mkArrow 
-				 (mkApp (eq, [|(mkRel 6);(mkRel 4)|]))
-				 (mkApp (eq, [|(mkRel 6);(mkRel 4)|])));
-			      (mkArrow
-				 (mkApp (eq, [|(mkRel 5);(mkRel 3)|]))
-				 (mkApp (eq, [|(mkRel 7);(mkRel 5)|])));
-			      (lambda_create env
-				 ((mkApp (eq, [|(mkRel 6);(mkRel 4)|])),
-				  (mkApp (trans,
-					  [|(mkRel 6);(mkRel 7);(mkRel 4);
-					    (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|]));
-					    (mkApp (trans,
-						    [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|]))));
-			      (lambda_create env
-				 ((mkApp (eq, [|(mkRel 5);(mkRel 3)|])),
-				  (mkApp (trans,
-					  [|(mkRel 7);(mkRel 6);(mkRel 5);(mkRel 3);
-					    (mkApp (trans,
-						    [|(mkRel 6);(mkRel 4);(mkRel 5);(mkRel 1);
-						      (mkApp (sym, [|(mkRel 5);(mkRel 4);(mkRel 2)|]))|]))|]))))|]))))))))
+let eq_lem2_proof env a eq sym trans =
+  let sign = eq_lem_common_sign env a eq in
+  let ccl1 =
+    mkArrow
+      (mkApp (eq, [|(mkRel 6);(mkRel 4)|]))
+      (mkApp (eq, [|(mkRel 6);(mkRel 4)|])) in
+  let ccl2 =
+    mkArrow
+      (mkApp (eq, [|(mkRel 5);(mkRel 3)|]))
+      (mkApp (eq, [|(mkRel 7);(mkRel 5)|])) in
+  let ccl = mkApp (Lazy.force coqand, [|ccl1;ccl2|]) in
+  let body =
+    mkApp ((Lazy.force coqconj),
+    [|ccl1;ccl2;
+      lambda_create env
+	(mkApp (eq, [|(mkRel 6);(mkRel 4)|]),
+	(mkApp (trans,
+	  [|(mkRel 6);(mkRel 7);(mkRel 4);
+	    (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|]));
+	    (mkApp (trans,
+	      [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|])));
+      lambda_create env
+        (mkApp (eq, [|(mkRel 5);(mkRel 3)|]),
+        (mkApp (trans,
+          [|(mkRel 7);(mkRel 6);(mkRel 5);(mkRel 3);
+            (mkApp (trans,
+              [|(mkRel 6);(mkRel 4);(mkRel 5);(mkRel 1);
+                (mkApp (sym, [|(mkRel 5);(mkRel 4);(mkRel 2)|]))|]))|])))|])
+  in
+  let p = it_mkLambda_or_LetIn body sign in
+  let t = it_mkProd_or_LetIn ccl sign in
+  (p,t)
 
 let gen_eq_lem_name =
   let i = ref 0 in
@@ -278,19 +288,19 @@ let add_setoid a aeq th =
 		     set_th = th}));
 	  let sym = mkApp ((Lazy.force coq_seq_sym), [|a; aeq; th|]) in
 	  let trans = mkApp ((Lazy.force coq_seq_trans), [|a; aeq; th|]) in
-	  let eq_morph = eq_lem_proof env a aeq sym trans in
-	  let eq_morph2 = eq_lem2_proof env a aeq sym trans in
+	  let (eq_morph, eq_morph_typ) = eq_lem_proof env a aeq sym trans in
+	  let (eq_morph2, eq_morph2_typ) = eq_lem2_proof env a aeq sym trans in
 	    Options.if_verbose ppnl (prterm a ++str " is registered as a setoid");
 	    let eq_ext_name = gen_eq_lem_name () in 
 	    let eq_ext_name2 = gen_eq_lem_name () in 
 	    let _ = Declare.declare_constant eq_ext_name
 		      ((DefinitionEntry {const_entry_body = eq_morph; 
-		                       const_entry_type = None;
+		                       const_entry_type = Some eq_morph_typ;
                                        const_entry_opaque = true}),
 		       Libnames.NeverDischarge) in
 	    let _ = Declare.declare_constant eq_ext_name2
 		      ((DefinitionEntry {const_entry_body = eq_morph2; 
-				       const_entry_type = None;
+				       const_entry_type = Some eq_morph2_typ;
                                        const_entry_opaque = true}),
 		       Libnames.NeverDischarge) in
 	    let eqmorph = (current_constant eq_ext_name) in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 09013d173..d3acbe66b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -263,7 +263,7 @@ let build_id_coercion idf_opt source =
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
       { const_entry_body = mkCast (val_f, typ_f);
-	const_entry_type = None;
+	const_entry_type = Some typ_f;
         const_entry_opaque = false } in
   let (_,kn) = declare_constant idf (constr_entry,NeverDischarge) in
   ConstRef kn
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a6e42a73a..a670c2bda 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -354,14 +354,11 @@ let build_recursive lnameargsardef =
   let n = NeverDischarge in 
   let recvec = 
     Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
+  let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
   let rec declare i fi =
     let ce = 
-      { const_entry_body =
-	  mkFix ((nvrec,i),
-	         (Array.map (fun id -> Name id) namerec,
-                  arrec,
-		  recvec));
-        const_entry_type = None;
+      { const_entry_body = mkFix ((nvrec,i),recdecls);
+        const_entry_type = Some arrec.(i);
         const_entry_opaque = false } in
     let (_,kn) = declare_constant fi (DefinitionEntry ce, n) in
     (ConstRef kn)
@@ -418,13 +415,11 @@ let build_corecursive lnameardef =
   let n = NeverDischarge in 
   let recvec = 
     Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
+  let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
   let rec declare i fi =
     let ce = 
-      { const_entry_body =
-	  mkCoFix (i, (Array.map (fun id -> Name id) namerec,
-                       arrec,
-		       recvec));
-        const_entry_type = None;
+      { const_entry_body = mkCoFix (i, recdecls);
+        const_entry_type = Some (arrec.(i));
         const_entry_opaque = false } 
     in
     let _,kn = declare_constant fi (DefinitionEntry ce,n) in
@@ -462,8 +457,10 @@ let build_scheme lnamedepindsort =
   let n = NeverDischarge in 
   let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in 
   let rec declare decl fi lrecref =
+    let decltype = Retyping.get_type_of env0 Evd.empty decl in
+    let decltype = Evarutil.refresh_universes decltype in
     let ce = { const_entry_body = decl;
-               const_entry_type = None;
+               const_entry_type = Some decltype;
                const_entry_opaque = false } in
     let _,kn = declare_constant fi (DefinitionEntry ce,n) in
     ConstRef kn :: lrecref
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ab3482c91..9edb4e1d5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -108,16 +108,14 @@ type field_status =
   | NoProjection of name
   | Projection of constr
 
-type projection_status =
-  | NotDefinable of identifier list
-  | Definable of constr
+exception NotDefinable of record_error
 
 (* This replaces previous projection bodies in current projection *)
 (* Undefined projs are collected and, at least one undefined proj occurs *)
 (* in the body of current projection then the latter can not be defined *)
 (* [c] is defined in ctxt [[params;fields]] and [l] is an instance of *)
 (* [[fields]] defined in ctxt [[params;x:ind]] *)
-let subst_projection l c =
+let subst_projection fid l c =
   let lv = List.length l in
   let bad_projs = ref [] in
   let rec substrec depth c = match kind_of_term c with
@@ -136,10 +134,9 @@ let subst_projection 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
-    NotDefinable (List.rev !bad_projs)
-  else 
-    Definable c''
+  if !bad_projs <> [] then 
+    raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
+  c''
 
 (* We build projections *)
 let declare_projections indsp coers fields =
@@ -158,54 +155,44 @@ let declare_projections indsp coers fields =
 	| Anonymous ->
 	    (nfi-1, None::sp_projs,NoProjection fi::subst)
 	| Name fid ->
-	  let abstract, c = match optci with
-	  | Some ci -> false, ci
-	  | None -> true, ti in
-	  match subst_projection subst c with
-	  | NotDefinable bad_projs ->
-	      warning_or_error coe indsp (MissingProj (fid,bad_projs));
-	      (nfi-1, None::sp_projs,NoProjection fi::subst)
-	  | Definable c' ->
-	    (* [c'] is defined in context [params;x:rp] *)
-	    let body =
-	      if abstract then
-		(* [c''] is defined in context [params;x:rp;x:rp] *)
-		let c'' = liftn 1 2 c' in
-		let p = mkLambda (x, lift 1 rp, c'') in
+            try
+              let ccl = subst_projection fid subst ti in
+	      let body = match optci with
+              | Some ci -> subst_projection fid subst ci
+              | None ->
+	        (* [ccl] is defined in context [params;x:rp] *)
+		(* [ccl'] is defined in context [params;x:rp;x:rp] *)
+		let ccl' = liftn 1 2 ccl in
+		let p = mkLambda (x, lift 1 rp, ccl') in
 		let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
 		let ci = Inductiveops.make_case_info env indsp
 		  (Some PrintLet) [| RegularPat |] in
-		mkCase (ci, p, mkRel 1, [|branch|])
-	      else c' in
-	    let proj =
-	      it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
-	    let name = 
-	      try
-		let cie = {
-		  const_entry_body = proj;
-                  const_entry_type = None;
-                  const_entry_opaque = false } in
-		let sp =
+		mkCase (ci, p, mkRel 1, [|branch|]) in
+	      let proj =
+	        it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
+              let projtyp =
+                it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
+	      let (sp,kn) =
+	        try
+		  let cie = {
+		    const_entry_body = proj;
+                    const_entry_type = Some projtyp;
+                    const_entry_opaque = false } in
 		  declare_constant fid (DefinitionEntry cie,NeverDischarge)
-		in Some sp
-              with Type_errors.TypeError (ctx,te) -> begin
-		warning_or_error coe indsp (BadTypedProj (fid,ctx,te));
-		None
-	     end in
-	   match name with
-	     | None ->
-		 (nfi-1, None::sp_projs, NoProjection fi::subst)
-	     | Some (sp,kn) ->
-		 let refi = ConstRef kn in
-		 let constr_fi = mkConst kn in
-		 if coe then begin
-		   let cl = Class.class_of_ref (IndRef indsp) in
-		   Class.try_add_new_coercion_with_source 
-		     refi NeverDischarge cl
-		 end;
-		 let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
-		 let constr_fip = applist (constr_fi,proj_args) in
-		 (nfi-1, (Some kn)::sp_projs, Projection constr_fip::subst))
+                with Type_errors.TypeError (ctx,te) ->
+                  raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
+	      let refi = ConstRef kn in
+	      let constr_fi = mkConst kn in
+	      if coe then begin
+	        let cl = Class.class_of_ref (IndRef indsp) in
+	        Class.try_add_new_coercion_with_source refi NeverDischarge cl
+	      end;
+	      let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
+	      let constr_fip = applist (constr_fi,proj_args) in
+	      (nfi-1, (Some kn)::sp_projs, Projection constr_fip::subst)
+            with NotDefinable why ->
+	      warning_or_error coe indsp why;
+	      (nfi-1, None::sp_projs,NoProjection fi::subst))
       (List.length fields,[],[]) coers (List.rev fields)
   in sp_projs