Do a second pass on the treatment of user-given implicit arguments. Now

works in inductive type definitions and fixpoints. The semantics of
an implicit inductive parameter is maybe a bit weird: it is implicit in the
inductive definition of constructors and the contructor types but not in
the inductive type itself (ie. to model the fact that one rarely wants A
in vector A n to be implicit but in vnil yes). Example in test-suite/
Also, correct the handling of the implicit arguments across sections. 
Every definition which had no explicitely given implicit arguments was
treated as if we asked to do global automatic implicit arguments on
section closing. Hence some arguments were given implicit status for no
apparent reason.
Also correct and test the parsing rule which disambiguates between {wf
..} and {A ..}.


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

12 files changed, 153 insertions, 63 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b06880bd3..9c40c861e 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -374,7 +374,7 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_context rec_sign env in
 
   (* Get interpretation metadatas *)
-  let impls = Command.compute_interning_datas env [] fixnames fixtypes in
+  let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in
   let notations = List.fold_right Option.List.cons ntnl [] in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 156d15566..49b719bdb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1144,17 +1144,36 @@ let intern_pattern env patt =
 let intern_ltac isarity ltacvars sigma env c =
   intern_gen isarity sigma env ~ltacvars:ltacvars c
 
+type manual_implicits = (explicitation * (bool * bool)) list
+
+let implicits_of_rawterm l = 
+  let rec aux i c = 
+    match c with
+	RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> 
+	  let rest = aux (succ i) b in
+	    if bk = Implicit then
+	      let name =
+		match na with
+		    Name id -> Some id
+		  | Anonymous -> None
+	      in
+		(ExplByPos (i, name), (true, true)) :: rest
+	    else rest
+      | RLetIn (loc, na, t, b) -> aux i b
+      | _ -> []
+  in aux 1 l
+
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
 let interp_gen kind sigma env 
                ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
-  Default.understand_gen kind sigma env 
-    (intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c)
+  let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
+    Default.understand_gen kind sigma env c
 
 let interp_constr sigma env c =
-  interp_gen (OfType None) sigma env c 
+  interp_gen (OfType None) sigma env c
 
 let interp_type sigma env ?(impls=([],[])) c =
   interp_gen IsType sigma env ~impls c
@@ -1168,9 +1187,20 @@ let interp_open_constr sigma env c =
 let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
+let interp_constr_evars_gen_impls evdref env ?(impls=([],[])) kind c =
+  let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+  let imps = implicits_of_rawterm c in
+    Default.understand_tcc_evars evdref env kind c, imps
+
 let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
-  Default.understand_tcc_evars evdref env kind
-    (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c)
+  let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+    Default.understand_tcc_evars evdref env kind c
+      
+let interp_casted_constr_evars_impls evdref env ?(impls=([],[])) c typ =
+  interp_constr_evars_gen_impls evdref env ~impls (OfType (Some typ)) c
+
+let interp_type_evars_impls evdref env ?(impls=([],[])) c =
+  interp_constr_evars_gen_impls evdref env IsType ~impls c
 
 let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f4272a2b1..9f3a815ee 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -45,6 +45,8 @@ type var_internalisation_data =
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
 
+type manual_implicits = (explicitation * (bool * bool)) list
+
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 (*s Internalisation performs interpretation of global names and notations *)
@@ -74,14 +76,22 @@ val interp_gen : typing_constraint -> evar_map -> env ->
 val interp_constr : evar_map -> env -> 
   constr_expr -> constr
 
-val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> 
-  constr_expr -> types -> constr
-
 val interp_type : evar_map -> env -> ?impls:full_implicits_env -> 
   constr_expr -> types
 
 val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
+val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> 
+  constr_expr -> types -> constr
+
+(* Accepting evars and giving back the manual implicits in addition. *)
+
+val interp_casted_constr_evars_impls : evar_defs ref -> env -> 
+  ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
+
+val interp_type_evars_impls : evar_defs ref -> env -> ?impls:full_implicits_env ->
+  constr_expr -> types * manual_implicits
+
 val interp_casted_constr_evars : evar_defs ref -> env -> 
   ?impls:full_implicits_env -> constr_expr -> types -> constr
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 081bb58c1..9ffd103de 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -471,9 +471,10 @@ let rebuild_implicits (req,l) =
       | ImplAuto -> [ref,compute_global_implicits flags ref]
       | ImplManual l -> 
 	  let auto = compute_global_implicits flags ref in
+	  let auto = if flags.main then auto else List.map (fun _ -> None) auto in
 	  let l' = merge_impls auto l in [ref,l']
   in (req,l')
-
+    
 
 let (inImplicits, _) =
   declare_object {(default_object "IMPLICITS") with 
@@ -530,6 +531,10 @@ let declare_manual_implicits local ref enriching l =
   in
     add_anonymous_leaf (inImplicits (req,[ref,l']))
 
+let maybe_declare_manual_implicits local ref enriching l =
+  if l = [] then ()
+  else declare_manual_implicits local ref enriching l
+
 (*s Registration as global tables *)
 
 let init () = implicits_table := Refmap.empty
diff --git a/library/impargs.mli b/library/impargs.mli
index a9e6ccb91..e7b05f422 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -57,7 +57,7 @@ val compute_implicits : env -> types -> implicits_list
 
 (* A [manual_explicitation] is a tuple of a positional or named explicitation with
    maximal insertion and forcing flags. *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool) 
+type manual_explicitation = Topconstr.explicitation * (bool * bool)
 
 val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list
 
@@ -69,8 +69,16 @@ val declare_mib_implicits : mutual_inductive -> unit
 
 val declare_implicits : bool -> global_reference -> unit
 
-(* Manual declaration of which arguments are expected implicit *)
+(* [declare_manual_implicits local ref enriching l]
+   Manual declaration of which arguments are expected implicit.
+   Unsets implicits if [l] is empty. *)
+
 val declare_manual_implicits : bool -> global_reference -> bool ->
   manual_explicitation list -> unit
 
+(* If the list is empty, do nothing, otherwise declare the implicits. *)
+
+val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
+  manual_explicitation list -> unit
+
 val implicits_of_global : global_reference -> implicits_list
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 68389c54a..423ade8b6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -103,13 +103,16 @@ let impl_ident =
   Gram.Entry.of_parser "impl_ident"
     (fun strm ->
       match Stream.npeek 1 strm with
-	| [("IDENT",("wf"|"struct"|"measure"))] ->
-	    raise Stream.Failure
-	| [("IDENT",s)] -> 
-	    Stream.junk strm;
-            Names.id_of_string s
+	| [(_,"{")] -> 
+	    (match Stream.npeek 2 strm with
+	      | [_;("IDENT",("wf"|"struct"|"measure"))] ->
+		  raise Stream.Failure
+	      | [_;("IDENT",s)] -> 
+		  Stream.junk strm; Stream.junk strm;
+		  Names.id_of_string s
+	      | _ -> raise Stream.Failure)
 	| _ -> raise Stream.Failure)
-
+    
 let ident_eq =
   Gram.Entry.of_parser "ident_eq"
     (fun strm ->
@@ -356,10 +359,26 @@ GEXTEND Gram
 	  ctx @ bl
     | cl = LIST0 binder_let -> cl ] ]
   ;
+  binder_assum:
+    [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
+    | idl=LIST1 name; ":"; c=lconstr; "}" ->
+        (fun id -> LocalRawAssum (id::idl,Default Implicit,c))
+    | idl=LIST1 name; "}" ->
+        (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (loc, None)))
+    | ":"; c=lconstr; "}" ->
+	(fun id -> LocalRawAssum ([id],Default Implicit,c))
+    ] ]
+  ;
+  fixannot:
+    [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
+    | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel)
+    | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel)
+    ] ]
+  ;
   binders_let_fixannot:
-    [ [ "{"; IDENT "struct"; id=name; "}" -> [], (Some id, CStructRec)
-    | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> [], (id, CWfRec rel)
-    | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> [], (id, CMeasureRec rel)
+    [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot -> 
+	(assum (loc, Name id) :: fst bl), snd bl
+    | f = fixannot -> [], f
     | b = binder_let; bl = binders_let_fixannot -> 
 	b :: fst bl, snd bl
     | -> [], (None, CStructRec)
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 024b32af4..39df21328 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -157,7 +157,7 @@ Section Well_founded_2.
    P x x' :=
     F
       (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
-         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a h)).
+         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)).
   End Acc_iter_2.
 
   Hypothesis Rwf : well_founded R.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 98b18f903..bf37c8f23 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -2,6 +2,8 @@ Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
 Require Import ProofIrrelevance.
 
+Implicit Arguments Enriching Acc_inv [y].
+
 (** Reformulation of the Wellfounded module using subsets where possible. *)
 
 Section Well_founded.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4af59ff62..3896f02dd 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -183,7 +183,7 @@ let declare_structure env id idbuild params arity fields =
       mind_entry_record = true;
       mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
-  let kn = Command.declare_mutual_with_eliminations true mie in
+  let kn = Command.declare_mutual_with_eliminations true mie [] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
   let kinds,sp_projs = Record.declare_projections rsp ~name:id (List.map (fun _ -> false) fields) fields in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 327fe904e..b5c9cb59b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -139,8 +139,7 @@ let red_constant_entry bl ce = function
 let declare_global_definition ident ce local imps =
   let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
   let gr = ConstRef kn in
-    if Impargs.is_implicit_args () || imps <> [] then
-      declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
     if local = Local && Flags.is_verbose() then
       msg_warning (pr_id ident ++ str" is declared as a global definition");
     definition_message ident;
@@ -192,8 +191,7 @@ let declare_one_assumption is_coe (local,kind) c imps nl (_,ident) =
         let kn =
           declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
 	let gr = ConstRef kn in
-	  if Impargs.is_implicit_args () || imps <> [] then
-	    declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+	  maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
         assumption_message ident;
         if local=Local & Flags.is_verbose () then
           msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -459,18 +457,18 @@ let declare_eliminations sp =
 
 (* 3b| Mutual inductive definitions *)
 
-let compute_interning_datas env l nal typl =
-  let mk_interning_data na typ =
+let compute_interning_datas env l nal typl impll =
+  let mk_interning_data na typ impls =
     let idl, impl =
-      if is_implicit_args() then
-	let impl = compute_implicits env typ in
-	let sub_impl,_ = list_chop (List.length l) impl in
-	let sub_impl' = List.filter is_status_implicit sub_impl in
+      let impl = 
+	compute_implicits_with_manual env typ (is_implicit_args ()) impls
+      in 
+      let sub_impl,_ = list_chop (List.length l) impl in
+      let sub_impl' = List.filter is_status_implicit sub_impl in
 	(List.map name_of_implicit sub_impl', impl)
-      else 
-	([],[]) in
-    (na, (idl, impl, compute_arguments_scope typ)) in
-  (l, List.map2 mk_interning_data nal typl)
+    in
+      (na, (idl, impl, compute_arguments_scope typ)) in
+  (l, list_map3 mk_interning_data nal typl impll)
 
 let declare_interning_data (_,impls) (df,c,scope) =
   silently (Metasyntax.add_notation_interpretation df impls c) scope
@@ -521,13 +519,14 @@ let interp_cstrs evdref env impls mldata arity ind =
   (* Complete conclusions of constructor types if given in ML-style syntax *)
   let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
   (* Interpret the constructor types *)
-  let ctyps'' = List.map (interp_type_evars evdref env ~impls) ctyps' in
-  (cnames, ctyps'')
+  let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in
+    (cnames, ctyps'', cimpls)
 
 let interp_mutual paramsl indl notations finite = 
   check_all_names_different indl;
   let env0 = Global.env() in
   let evdref = ref (Evd.create_evar_defs Evd.empty) in
+  let userimpls = Implicit_quantifiers.implicits_of_binders paramsl in
   let env_params, ctx_params = interp_context_evars evdref env0 paramsl in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
@@ -542,7 +541,8 @@ let interp_mutual paramsl indl notations finite =
   let env_ar_params = push_rel_context ctx_params env_ar in
 
   (* Compute interpretation metadatas *)
-  let impls = compute_interning_datas env0 params indnames fullarities in
+  let indimpls = List.map (fun _ -> userimpls) fullarities in
+  let impls = compute_interning_datas env0 params indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
@@ -556,17 +556,17 @@ let interp_mutual paramsl indl notations finite =
   (* Instantiate evars and check all are resolved *)
   let evd,_ = consider_remaining_unif_problems env_params !evdref in
   let sigma = evars_of evd in
-  let constructors = List.map (fun (idl,cl) -> (idl,List.map (nf_evar sigma) cl)) constructors in
+  let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
   let arities = List.map (nf_evar sigma) arities in
   List.iter (check_evars env_params Evd.empty evd) arities;
   Sign.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
-  List.iter (fun (_,ctyps) ->
+  List.iter (fun (_,ctyps,_) ->
     List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
     constructors;
   
   (* Build the inductive entries *)
-  let entries = list_map3 (fun ind arity (cnames,ctypes) -> {
+  let entries = list_map3 (fun ind arity (cnames,ctypes,cimpls) -> {
     mind_entry_typename = ind.ind_name;
     mind_entry_arity = arity;
     mind_entry_consnames = cnames;
@@ -577,7 +577,7 @@ let interp_mutual paramsl indl notations finite =
   { mind_entry_params = List.map prepare_param ctx_params;
     mind_entry_record = false; 
     mind_entry_finite = finite; 
-    mind_entry_inds = entries }
+    mind_entry_inds = entries }, (List.map (fun (_,_,impls) -> userimpls, impls) constructors)
 
 let eq_constr_expr c1 c2 =
   try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false
@@ -630,21 +630,36 @@ let _ =
       optwrite = (fun b -> elim_flag := b) }
 
 
-let declare_mutual_with_eliminations isrecord mie =
+let lift_implicits n = 
+  List.map (fun x -> 
+    match fst x with 
+	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
+      | _ -> x)
+
+let declare_mutual_with_eliminations isrecord mie impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
-  let (_,kn) = declare_mind isrecord mie in
-  if_verbose ppnl (minductive_message names);
-  if !elim_flag then declare_eliminations kn;
-  kn
+  let params = List.length mie.mind_entry_params in
+  let (_,kn) = declare_mind isrecord mie in    
+    list_iter_i (fun i (indimpls, constrimpls) -> 
+      let ind = (kn,i) in
+	list_iter_i
+	  (fun j impls -> 
+	    maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
+	      (is_implicit_args()) (indimpls @ (lift_implicits params impls)))
+	  constrimpls)
+      impls;
+    if_verbose ppnl (minductive_message names);
+    if !elim_flag then declare_eliminations kn;
+    kn
 
 let build_mutual l finite =
   let indl,ntnl = List.split l in
   let paramsl = extract_params indl in
   let coes = extract_coercions indl in
   let notations,indl = prepare_inductive ntnl indl in
-  let mie = interp_mutual paramsl indl notations finite in
+  let mie,impls = interp_mutual paramsl indl notations finite in
   (* Declare the mutual inductive block with its eliminations *)
-  ignore (declare_mutual_with_eliminations false mie);
+  ignore (declare_mutual_with_eliminations false mie impls);
   (* Declare the possible notations of inductive types *)
   List.iter (declare_interning_data ([],[])) notations;
   (* Declare the coercions *)
@@ -785,11 +800,9 @@ let declare_fix boxed kind f def t imps =
   } in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
   let gr = ConstRef kn in
-    if Impargs.is_implicit_args () || imps <> [] then
-      declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
     gr
-
-
+      
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
   let names = List.map (fun id -> Name id) fixnames in
@@ -828,7 +841,7 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_types env fixnames fixtypes in
 
   (* Get interpretation metadatas *)
-  let impls = compute_interning_datas env [] fixnames fixtypes in
+  let impls = compute_interning_datas env [] fixnames fixtypes fiximps in
   let notations = List.fold_right Option.List.cons ntnl [] in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
@@ -1043,8 +1056,7 @@ let start_proof_com sopt kind (bl,t) hook =
   let j = Default.understand_judgment sigma env ib in
     start_proof id kind j.uj_val
       (fun str cst -> 
-	if Impargs.is_implicit_args () || imps <> [] then
-	  declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
+	maybe_declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
 	hook str cst)
 
 let check_anonymity id save_ident =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d67daa83a..a6a403c03 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -57,16 +57,20 @@ val compute_interning_datas :  Environ.env ->
     'a list ->
     'b list ->
     Term.types list ->
-    'a list *
+    Impargs.manual_explicitation list list ->
+  'a list *
     ('b *
-     (Names.identifier list * Impargs.implicits_list *
-      Topconstr.scope_name option list))
+	(Names.identifier list * Impargs.implicits_list *
+	    Topconstr.scope_name option list))
     list
 
 val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
 
 val declare_mutual_with_eliminations :
-  bool -> Entries.mutual_inductive_entry -> mutual_inductive
+  bool -> Entries.mutual_inductive_entry -> 
+  (Impargs.manual_explicitation list *
+      Impargs.manual_explicitation list list) list ->
+  mutual_inductive
 
 type fixpoint_kind =
   | IsFixpoint of (int option * recursion_order_expr) list
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b04557304..57a7e63b3 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -223,7 +223,7 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
       mind_entry_record = true;
       mind_entry_finite = not declare_as_coind;
       mind_entry_inds = [mie_ind] } in
-  let kn = declare_mutual_with_eliminations true mie in
+  let kn = declare_mutual_with_eliminations true mie [] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let kinds,sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)