Moving centralised discharge into dispatched discharge_function; required to delay some computation from before to after caching time + exporting whether a projection is a true projection or a constant associated to a let in the type of the record constructor (fix a bug for canonical structures with let's)

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

2 files changed, 16 insertions, 14 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index c05220989..f6d8b6000 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -152,13 +152,14 @@ let declare_projections indsp coers fields =
   let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
   let x = Termops.named_hd (Global.env()) r Anonymous in
   let lifted_fields = lift_rel_context 1 fields in
-  let (_,sp_projs,_) =
+  let (_,kinds,sp_projs,_) =
     List.fold_left2
-      (fun (nfi,sp_projs,subst) coe (fi,optci,ti) ->
-	match fi with
-	| Anonymous ->
-	    (nfi-1, None::sp_projs,NoProjection fi::subst)
-	| Name fid ->
+      (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) ->
+	let (sp_projs,subst) =
+	  match fi with
+	  | Anonymous ->
+	      (None::sp_projs,NoProjection fi::subst)
+	  | Name fid ->
             try
               let ccl = subst_projection fid subst ti in
 	      let body = match optci with
@@ -192,17 +193,18 @@ let declare_projections indsp coers fields =
 	      let refi = ConstRef kn in
 	      let constr_fi = mkConst kn in
 	      if coe then begin
-	        let cl = Class.class_of_ref (IndRef indsp) in
+	        let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi Global 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)
+	      (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
+	      (None::sp_projs,NoProjection fi::subst) in
+      (nfi-1,(optci=None)::kinds,sp_projs,subst))
+      (List.length fields,[],[],[]) coers (List.rev fields)
+  in (kinds,sp_projs)
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
    list telling if the corresponding fields must me declared as coercion *)
@@ -232,7 +234,7 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
       mind_entry_inds = [mie_ind] } in
   let sp = declare_mutual_with_eliminations true mie in
   let rsp = (sp,0) in (* This is ind path of idstruc *)
-  let sp_projs = declare_projections rsp coers fields in
+  let kinds,sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
   if is_coe then Class.try_add_new_coercion build Global;
-  Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs)
+  Recordops.declare_structure(rsp,idbuild,nparams,List.rev kinds,List.rev sp_projs)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index b8a1a6ce6..5074719bc 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -21,7 +21,7 @@ open Topconstr
    [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> bool list -> rel_context -> constant option list
+  inductive -> bool list -> rel_context -> bool list * constant option list
 
 val definition_structure :
   lident with_coercion * local_binder list *