Ré-introduction des implicites à la volée dans la définition des inductifs

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

1 files changed, 12 insertions, 5 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 02f1635e9..49dd7b887 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -171,21 +171,28 @@ let interp_mutual lparams lnamearconstrs finite =
 		  | Anonymous -> anomaly "Unnamed inductive variable"
 		in (id, LocalAssum p)) params
   in
-  let (ind_env,arityl) =
+  let (ind_env,ind_impls,arityl) =
     List.fold_left
-      (fun (env,arl) (recname,arityc,_) ->
+      (fun (env, ind_impls, arl) (recname, arityc,_) ->
          let arity = interp_type sigma env_params arityc in
 	 let fullarity = prod_it arity params in
 	 let env' = Environ.push_rel_assum (Name recname,fullarity) env in
-	 (env', (arity::arl)))
-      (env0,[]) lnamearconstrs
+	 let impls = 
+	   if Impargs.is_implicit_args()
+	   then Impargs.compute_implicits env_params sigma fullarity
+	   else [] in
+	 (env', (recname,impls)::ind_impls, (arity::arl)))
+      (env0, [], []) lnamearconstrs
   in
   let ind_env_params = Environ.push_rels_assum params ind_env in
   let mispecvec = 
     List.map2
       (fun ar (name,_,lname_constr) ->
 	 let constrnames, bodies = List.split lname_constr in
-         let constrs = List.map (interp_constr sigma ind_env_params) bodies in
+         let constrs =
+	   List.map 
+	     (interp_type_with_implicits sigma ind_env_params ind_impls) bodies
+	 in
 	 { mind_entry_nparams = nparams;
 	   mind_entry_params = params';
 	   mind_entry_typename = name;