first attempt to allow Function to deal with dependent pattern matching. This Functionnality is VERY VERY experimental and only works with non recursive functions and structurally defined function

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

6 files changed, 337 insertions, 107 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 6241eb1de..903136ca2 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -59,9 +59,9 @@ let list_chop ?(msg="") n l =
     failwith (msg ^ msg')
   
 
-let make_refl_eq type_of_t t  =
-  let refl_equal_term = Lazy.force refl_equal in
-  mkApp(refl_equal_term,[|type_of_t;t|])
+let make_refl_eq constructor type_of_t t  =
+(*   let refl_equal_term = Lazy.force refl_equal in *)
+  mkApp(constructor,[|type_of_t;t|])
 
 
 type pte_info = 
@@ -109,11 +109,19 @@ let intro_erasing id = tclTHEN (thin [id]) (introduction id)
 let rec_hyp_id = id_of_string "rec_hyp"
 
 let is_trivial_eq t = 
-  match kind_of_term t with 
-    | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
-	eq_constr t1 t2
-    | _ -> false 
-
+  let res =   try 
+    begin
+      match kind_of_term t with 
+	| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
+	    eq_constr t1 t2
+	| App(f,[|t1;a1;t2;a2|]) when eq_constr f (jmeq ())  ->
+	    eq_constr t1 t2 && eq_constr a1 a2
+	| _ -> false 
+    end
+  with _ -> false
+  in
+(*   observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
+  res
 
 let rec incompatible_constructor_terms t1 t2 = 
   let c1,arg1 = decompose_app t1 
@@ -127,10 +135,19 @@ let rec incompatible_constructor_terms t1 t2 =
     )
 
 let is_incompatible_eq t = 
-  match kind_of_term t with 
-    | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
-	incompatible_constructor_terms t1 t2
-    | _ -> false 
+  let res =
+    try
+      match kind_of_term t with 
+	| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
+	    incompatible_constructor_terms t1 t2
+	| App(f,[|u1;t1;u2;t2|]) when eq_constr f (jmeq ()) -> 
+	    (eq_constr u1 u2 &&
+	       incompatible_constructor_terms t1 t2)
+	| _ -> false 
+    with _ -> false
+  in 
+  if res then   observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
+  res
 
 let change_hyp_with_using msg hyp_id t tac : tactic = 
   fun g -> 
@@ -146,7 +163,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
 exception TOREMOVE
 
 
-let prove_trivial_eq h_id context (type_of_term,term) = 
+let prove_trivial_eq h_id context (constructor,type_of_term,term) = 
   let nb_intros = List.length context in 
   tclTHENLIST
     [
@@ -156,7 +173,7 @@ let prove_trivial_eq h_id context (type_of_term,term) =
 	   fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) 
 	 in
 	 let context_hyps' = 
-	   (mkApp(Lazy.force refl_equal,[|type_of_term;term|]))::
+	   (mkApp(constructor,[|type_of_term;term|]))::
 	     (List.map mkVar context_hyps)
 	 in
 	 let to_refine = applist(mkVar h_id,List.rev context_hyps') in 
@@ -165,10 +182,21 @@ let prove_trivial_eq h_id context (type_of_term,term) =
     ]
 
 
-let isAppConstruct t = 
-  if isApp t 
-  then isConstruct (fst (destApp t))
-  else false 
+
+let find_rectype env c =
+  let (t, l) = decompose_app (Reduction.whd_betadeltaiota env c) in
+  match kind_of_term t with
+  | Ind ind -> (t, l)
+  | Construct _ -> (t,l)
+  | _ -> raise Not_found
+
+
+let isAppConstruct ?(env=Global.env ()) t = 
+  try 
+    let t',l = find_rectype (Global.env ()) t in 
+    observe (str "isAppConstruct : " ++ Printer.pr_lconstr t ++ str " -> " ++ Printer.pr_lconstr (applist  (t',l)));
+    true
+  with Not_found -> false 
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
   let clos_norm_flags flgs env sigma t =
@@ -176,10 +204,11 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
   clos_norm_flags Closure.betaiotazeta  Environ.empty_env Evd.empty
     
 
+
 let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  = 
-  let nochange msg  = 
+  let nochange ?t' msg  = 
     begin 
-(*       observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t    ); *)
+      observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
       failwith "NoChange"; 
     end
   in    
@@ -188,12 +217,23 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  =
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp t) then nochange "not an equality";
     let f_eq,args = destApp t in
-    if not (eq_constr f_eq (Lazy.force eq)) then nochange "not an equality";
-    let t1 = args.(1) 
-    and t2 = args.(2) 
-    and t1_typ = args.(0)
+    let constructor,t1,t2,t1_typ = 
+      try 
+	if (eq_constr f_eq (Lazy.force eq)) 
+	then 
+	  let t1 = (args.(1),args.(0))
+	  and t2 = (args.(2),args.(0)) 
+	  and t1_typ = args.(0)
+	  in
+	  (Lazy.force refl_equal,t1,t2,t1_typ)
+	else
+	  if (eq_constr f_eq (jmeq ())) 
+	  then 
+	    (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0))
+	  else nochange "not an equality"
+      with _ -> nochange "not an equality"
     in 
-    if not (closed0 t1) then nochange "not a closed lhs";    
+    if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";    
     let rec compute_substitution sub t1 t2 = 
 (*       observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); *)
       if isRel t2 
@@ -211,16 +251,17 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  =
       else if isAppConstruct t1 && isAppConstruct t2 
       then 
 	begin
-	  let c1,args1 = destApp t1 
-	  and c2,args2 = destApp t2 
+	  let c1,args1 =  find_rectype env t1
+	  and c2,args2 = find_rectype env t2
 	  in 
-	  if not (eq_constr c1 c2) then anomaly "deconstructing equation";
-	  array_fold_left2 compute_substitution sub args1 args2
+	  if not (eq_constr c1 c2) then nochange "cannot solve (diff)";
+	  List.fold_left2 compute_substitution sub args1 args2
 	end
       else 
-	if (eq_constr t1 t2) then sub else nochange "cannot solve"
+	if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2)  "cannot solve (diff)"
     in
-    let sub = compute_substitution Intmap.empty t1 t2 in 
+    let sub = compute_substitution Intmap.empty (snd t1) (snd t2) in 
+    let sub = compute_substitution sub (fst t1) (fst t2) in
     let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) 
     let new_end_of_type = 
       (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 
@@ -234,7 +275,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  =
     in
     let old_context_length = List.length context + 1 in
     let witness_fun = 
-      mkLetIn(Anonymous,make_refl_eq t1_typ t1,t,
+      mkLetIn(Anonymous,make_refl_eq constructor t1_typ (fst t1),t,
 	       mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i)))
 	      )
     in
@@ -450,14 +491,20 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	  let real_type_of_hyp =
 	    it_mkProd_or_LetIn ~init:popped_t' context
 	  in
-	  let _,args = destApp t_x in
+	  let hd,args = destApp t_x in
+	  let get_args hd args = 
+	    if eq_constr hd (Lazy.force eq) 
+	    then (Lazy.force refl_equal,args.(0),args.(1))
+	    else (jmeq_refl (),args.(0),args.(1))
+	  in
 	  tclTHENLIST
 	    [
 	      change_hyp_with_using
 		"prove_trivial_eq"
 		hyp_id
 		real_type_of_hyp
-		((* observe_tac "prove_trivial_eq" *) (prove_trivial_eq hyp_id context (args.(0),args.(1))));
+		((* observe_tac "prove_trivial_eq" *) 
+		  (prove_trivial_eq hyp_id context (get_args hd args)));
 	      scan_type context popped_t'
 	    ] 
 	else 
@@ -631,28 +678,32 @@ let build_proof
 		  let g_nb_prod = nb_prod (pf_concl g) in
 		  let type_of_term = pf_type_of g t in
 		  let term_eq =
-		    make_refl_eq type_of_term t
+		    make_refl_eq (Lazy.force refl_equal) type_of_term t
 		  in
 		  tclTHENSEQ
 		    [
 		      h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
 		      thin dyn_infos.rec_hyps;
 		      pattern_option [(false,[1]),t] None;
-		      h_simplest_case t;
-		      (fun g' -> 
-			 let g'_nb_prod = nb_prod (pf_concl g') in 
-			 let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
-			 		     observe_tac "treat_new_case"
-			 (treat_new_case  
-			    ptes_infos
-			    nb_instanciate_partial 
-			    (build_proof do_finalize) 
-			    t 
-			    dyn_infos)
-			   g'
-		      )
+		      (fun g -> observe_tac "toto" (    
+			 tclTHENSEQ [h_simplest_case t;
+				     (fun g' -> 
+					let g'_nb_prod = nb_prod (pf_concl g') in 
+					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
+			 		observe_tac "treat_new_case"
+					  (treat_new_case  
+					     ptes_infos
+					     nb_instanciate_partial 
+					     (build_proof do_finalize) 
+					     t 
+					     dyn_infos)
+					  g'
+				     )
 			
-		    ] g
+				    ]) g
+		      )
+		    ]
+		    g
 	      in
 	      build_proof do_finalize_t {dyn_infos with info = t} g
 	  | Lambda(n,t,b) ->
@@ -1206,7 +1257,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 			    nb_rec_hyps = List.length branches
 			 }
 		       in
-		       (* observe_tac "cleaning" *) (clean_goal_with_heq
+		       observe_tac "cleaning" (clean_goal_with_heq
 			 (Idmap.map prove_rec_hyp ptes_to_fix) 
 			 do_prove 
 			 dyn_infos)
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index b03bdf31a..5155e614d 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -328,7 +328,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   in
   (*    let time2 = System.get_time ()  in *)
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
-  (*    observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
+     observe (str "new_principle_type : " ++ pr_lconstr new_principle_type);
   let new_princ_name =
     next_global_ident_away true (id_of_string "___________princ_________") []
   in
@@ -356,6 +356,7 @@ let generate_functional_principle
     old_princ_type sorts new_princ_name funs i proof_tac
     =
   try 
+    
   let f = funs.(i) in
   let type_sort = Termops.new_sort_in_family InType in
   let new_sorts =
@@ -718,9 +719,10 @@ let build_case_scheme fa =
   in
   let princ_name =  (fun (x,_,_) -> x) fa in
   let _ = 
-(*     observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
-(* 	       pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
-(* 	    ); *)
+  (*  Pp.msgnl (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++
+	       pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs
+	    );
+  *)
     generate_functional_principle
       false
       scheme_type
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index b6b2cbd11..d7a7c311a 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -272,26 +272,36 @@ let derive_inversion fix_names =
   with _ -> ()
 
 let warning_error names e = 
+  let e_explain e = 
+    match e with 
+      | ToShow e -> spc () ++ Cerrors.explain_exn e
+      | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+  in		
   match e with 
     | Building_graph e -> 
 	Pp.msg_warning 
 	  (str "Cannot define graph(s) for " ++ 
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	     if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+	     e_explain e)
     | Defining_principle e -> 
 	Pp.msg_warning
 	  (str "Cannot define principle(s) for "++ 
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	     if do_observe () then Cerrors.explain_exn e else mt ())
+	     e_explain e)
     | _ -> anomaly ""
 
 let error_error names e = 
+  let e_explain e = 
+    match e with 
+      | ToShow e -> spc () ++ Cerrors.explain_exn e
+      | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+  in
   match e with 
     | Building_graph e -> 
 	errorlabstrm ""  
 	  (str "Cannot define graph(s) for " ++ 
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	     if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+	     e_explain e)
     | _ -> anomaly ""
 
 let generate_principle  on_error
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 4892128a0..69cc0607b 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -524,3 +524,27 @@ let _ = declare_bool_option strict_tcc_sig
 
 exception Building_graph of exn 
 exception Defining_principle of exn
+exception ToShow of exn
+
+let init_constant dir s = 
+  try 
+    Coqlib.gen_constant "Function" dir s
+  with e -> raise (ToShow e)
+
+let jmeq () =   
+  try 
+    (Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; 
+     init_constant ["Logic";"JMeq"] "JMeq")
+  with e -> raise (ToShow e)
+
+let jmeq_rec () = 
+  try
+    Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; 
+	  init_constant ["Logic";"JMeq"] "JMeq_rec"
+  with e -> raise (ToShow e)
+
+let jmeq_refl () = 
+  try 
+    Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
+    init_constant ["Logic";"JMeq"] "JMeq_refl"
+  with e -> raise (ToShow e)
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 2d741f0b3..e9aa692b6 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -45,7 +45,8 @@ val def_of_const : Term.constr -> Term.constr
 val eq : Term.constr Lazy.t
 val refl_equal : Term.constr Lazy.t
 val const_of_id: identifier -> constant
-
+val jmeq : unit -> Term.constr
+val jmeq_refl : unit -> Term.constr 
 
 (* [save_named] is a copy of [Command.save_named] but uses 
    [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast] 
@@ -114,5 +115,6 @@ val do_observe : unit -> bool
 (* To localize pb *)
 exception Building_graph of exn 
 exception Defining_principle of exn
+exception ToShow of exn 
 
 val is_strict_tcc : unit -> bool
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 75f6207fc..d54aca4e6 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -25,7 +25,6 @@ type binder_type =
 
 type raw_context = (binder_type*rawconstr) list
 
-
 (* 
    compose_raw_context [(bt_1,n_1,t_1);......] rt returns 
    b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the 
@@ -712,20 +711,25 @@ and build_entry_lc_from_case env funname make_discr
 	    el
 	      (mk_result [] [] avoid)
 	in
-	(****** The next works only if the match is not dependent ****)
 	let types = 
 	  List.map (fun (case_arg,_) -> 
 		      let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in 
 		      Typing.type_of env Evd.empty case_arg_as_constr
 		   ) el
 	in
+	(****** The next works only if the match is not dependent ****)
 	let results =
 	  List.map 
-	    (build_entry_lc_from_case_term
+	    (fun ca -> 
+	       let res = build_entry_lc_from_case_term
 	       env types
-	       funname (make_discr (* (List.map fst el) *))
+	       funname (make_discr)
 	       []  brl 
-	       case_resl.to_avoid) 
+	       case_resl.to_avoid
+	       ca
+	       in 
+	       res
+	    ) 
 	    case_resl.result 
 	in 
 	{ 
@@ -754,14 +758,17 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		 let pat_ids = get_pattern_id renamed_pat  in 
 		 let env_with_pat_ids = add_pat_variables pat typ new_env in 
 		   List.fold_right 
-		   (fun id acc -> 		 
-		      let typ_of_id = Typing.type_of env_with_pat_ids Evd.empty (mkVar id) in 
-		      let raw_typ_of_id = 
-			Detyping.detype false [] (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
-		      in
-		      mkRProd (Name id,raw_typ_of_id,acc))
-		   pat_ids
-		   (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
+		     (fun id acc -> 		 
+			let typ_of_id = 
+			  Typing.type_of env_with_pat_ids Evd.empty (mkVar id) 
+			in 
+			let raw_typ_of_id = 
+			  Detyping.detype false [] 
+			    (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
+			in
+			mkRProd (Name id,raw_typ_of_id,acc))
+		     pat_ids
+		     (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
 	    )
 	    patl
 	    types
@@ -790,7 +797,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	    matched_expr
 	in
 	(* We now create the precondition of this branch i.e.
-
 	   1- the list of variable appearing in the different patterns of this branch and 
 	      the list of equation stating than el = patl (List.flatten ...)
 	   2- If there exists a previous branch which pattern unify with the one of this branch 
@@ -815,7 +821,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      raw_typ_of_id
 			   )::acc
 		      else acc
-			
 		   )
 		   idl
 		   [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)]
@@ -863,7 +868,9 @@ let is_res id =
    rebuild the raw constructors expression. 
    eliminates some meaningless equalities, applies some rewrites......
 *)
-let rec rebuild_cons nb_args relname args crossed_types depth rt = 
+let rec rebuild_cons env nb_args relname args crossed_types depth rt = 
+  observe (str "rebuilding : " ++ pr_rawconstr rt);
+
   match rt with 
     | RProd(_,n,k,t,b) -> 
 	let not_free_in_t id = not (is_free_in id t) in 
@@ -874,50 +881,147 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 		begin
 		  match args' with 
 		    | (RVar(_,this_relname))::args' -> 
-			let new_b,id_to_exclude =  
-			  rebuild_cons 
-			    nb_args relname
-			    args new_crossed_types
-			    (depth + 1) b
-			in 
-			(*i The next call to mk_rel_id is valid since we are constructing the graph
+			(*i The next call to mk_rel_id is 
+			  valid since we are constructing the graph
 			  Ensures by: obvious
 			  i*) 
 
 			let new_t = 
 			  mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt]) 
-			in mkRProd(n,new_t,new_b),
+			in 
+			let t' = Pretyping.Default.understand Evd.empty env new_t in 
+			let new_env = Environ.push_rel (n,None,t') env in 
+			let new_b,id_to_exclude =  
+			  rebuild_cons new_env
+			    nb_args relname
+			    args new_crossed_types
+			    (depth + 1) b
+			in 
+			mkRProd(n,new_t,new_b),
 			Idset.filter not_free_in_t id_to_exclude
 		    | _ -> (* the first args is the name of the function! *)
 			assert false 
 		end
-	    | RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt]) 
+	    | RApp(loc1,RRef(loc2,eq_as_ref),[ty;RVar(loc3,id);rt]) 
 		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
 		  -> 
-		let is_in_b = is_free_in id b in
-		let _keep_eq = 
-		  not (List.exists (is_free_in id) args) || is_in_b  || 
-		    List.exists (is_free_in id) crossed_types 
-		in 
-		let new_args = List.map (replace_var_by_term id rt) args in 
-		let subst_b = 
-		  if is_in_b then b else  replace_var_by_term id rt b 
-		in 
-		let new_b,id_to_exclude =  
-		  rebuild_cons 
-		    nb_args relname
-		    new_args new_crossed_types
-		    (depth + 1) subst_b
-		in 
-		mkRProd(n,t,new_b),id_to_exclude
+		begin
+		  try 
+		    observe (str "computing new type for eq : " ++ pr_rawconstr rt);
+		    let t' = Pretyping.Default.understand Evd.empty env t in
+		    let is_in_b = is_free_in id b in
+		    let _keep_eq = 
+		      not (List.exists (is_free_in id) args) || is_in_b  || 
+			List.exists (is_free_in id) crossed_types 
+		    in 
+		    let new_args = List.map (replace_var_by_term id rt) args in 
+		    let subst_b = 
+		      if is_in_b then b else  replace_var_by_term id rt b 
+		    in 
+		    let new_env = Environ.push_rel (n,None,t') env in
+		    let new_b,id_to_exclude =  
+		      rebuild_cons 
+			new_env
+			nb_args relname
+			new_args new_crossed_types
+			(depth + 1) subst_b
+		    in 
+		    mkRProd(n,t,new_b),id_to_exclude
+		  with _ -> 
+		    let jmeq = Libnames.IndRef (destInd (jmeq ())) in 
+		    let ty' = Pretyping.Default.understand Evd.empty env ty in 
+		    let ind,args' = Inductive.find_inductive env ty' in 
+		    let mib,_ = Global.lookup_inductive ind in 
+		    let nparam = mib.Declarations.mind_nparams in 
+		    let params,arg' = 
+		      ((Util.list_chop nparam args'))
+		    in
+		    let rt_typ = 
+		       RApp(Util.dummy_loc,
+			    RRef (Util.dummy_loc,Libnames.IndRef ind), 
+			    (List.map 
+			      (fun p -> Detyping.detype false [] 
+				 (Termops.names_of_rel_context env)
+				 p) params)@(Array.to_list 
+				      (Array.make 
+					 (List.length args' - nparam) 
+					 (mkRHole ()))))
+		    in
+		    let eq' = 
+		      RApp(loc1,RRef(loc2,jmeq),[ty;RVar(loc3,id);rt_typ;rt])
+		    in
+		    observe (str "computing new type for jmeq : " ++ pr_rawconstr eq');
+		    let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in
+		    observe (str " computing new type for jmeq : done") ;
+		    let new_args = 
+		      match kind_of_term eq'_as_constr with 
+			| App(_,[|_;_;ty;_|]) -> 
+			    let ty = Array.to_list (snd (destApp ty)) in 
+			    let ty' = snd (Util.list_chop nparam ty) in 
+			    List.fold_left2 
+			      (fun acc var_as_constr arg -> 
+				 if isRel var_as_constr 
+				 then 
+				   let (na,_,_) = 
+				     Environ.lookup_rel (destRel var_as_constr) env
+				   in 
+				   match na with 
+				     | Anonymous -> acc 
+				     | Name id' -> 
+					 (id',Detyping.detype false [] 
+					    (Termops.names_of_rel_context env)
+					    arg)::acc
+				 else if isVar var_as_constr 
+				 then (destVar var_as_constr,Detyping.detype false [] 
+					 (Termops.names_of_rel_context env)
+					 arg)::acc
+				 else acc
+			      )
+			      []
+			      arg'
+			      ty' 
+			| _ -> assert false
+		    in
+		    let is_in_b = is_free_in id b in
+		    let _keep_eq = 
+		      not (List.exists (is_free_in id) args) || is_in_b  || 
+			List.exists (is_free_in id) crossed_types 
+		    in 
+		    let new_args = 
+		      List.fold_left 
+			(fun args (id,rt) ->
+			   List.map (replace_var_by_term id rt) args
+			)
+			args 
+			((id,rt)::new_args)
+		    in 
+		    let subst_b = 
+		     if is_in_b then b else  replace_var_by_term id rt b
+		    in 
+		    let new_env = 
+		      let t' = Pretyping.Default.understand Evd.empty env eq' in 
+		      Environ.push_rel (n,None,t') env
+		    in
+		    let new_b,id_to_exclude =  
+		      rebuild_cons 
+			new_env
+			nb_args relname
+			new_args new_crossed_types
+			(depth + 1) subst_b
+		    in 
+		    mkRProd(n,eq',new_b),id_to_exclude
+		end
 		  (* J.F:. keep this comment  it explain how to remove some meaningless equalities 
 		     if keep_eq then
 		     mkRProd(n,t,new_b),id_to_exclude
 		     else new_b, Idset.add id id_to_exclude
 		  *)
 	    | _ -> 
+		observe (str "computing new type for prod : " ++ pr_rawconstr rt);
+		let t' = Pretyping.Default.understand Evd.empty env t in 
+		let new_env = Environ.push_rel (n,None,t') env in 
 		let new_b,id_to_exclude =  
-		  rebuild_cons 
+		  rebuild_cons new_env
 		    nb_args relname
 		    args new_crossed_types
 		    (depth + 1) b
@@ -932,10 +1036,13 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
+	  observe (str "computing new type for lambda : " ++ pr_rawconstr rt);
+	  let t' = Pretyping.Default.understand Evd.empty env t in 
 	  match n with
 	    | Name id ->
+		let new_env = Environ.push_rel (n,None,t') env in 
 		let new_b,id_to_exclude = 
-		  rebuild_cons 
+		  rebuild_cons new_env
 		    nb_args relname
 		    (args@[mkRVar id])new_crossed_types
 		    (depth + 1 ) b 
@@ -952,8 +1059,11 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
     | RLetIn(_,n,t,b) -> 
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in 
+	  let t' = Pretyping.Default.understand Evd.empty env t in 
+	  let type_t' = Typing.type_of env Evd.empty t' in 
+	  let new_env = Environ.push_rel (n,Some t',type_t') env in
 	  let new_b,id_to_exclude = 
-	    rebuild_cons 
+	    rebuild_cons new_env 
 	      nb_args relname
 	      args (t::crossed_types)
 	      (depth + 1 ) b in
@@ -968,14 +1078,16 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in 
 	  let new_t,id_to_exclude' = 
-	    rebuild_cons 
+	    rebuild_cons env
 	      nb_args
 	      relname 
 	      args (crossed_types) 
 	      depth t 
 	  in
+	  let t' = Pretyping.Default.understand Evd.empty env new_t in 
+	  let new_env = Environ.push_rel (na,None,t') env in 
 	  let new_b,id_to_exclude = 
-	    rebuild_cons 
+	    rebuild_cons new_env
 	      nb_args relname
 	      args (t::crossed_types) 
 	      (depth + 1) b 
@@ -993,11 +1105,11 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 
 
 (* debuging wrapper *)
-let rebuild_cons nb_args relname args crossed_types rt = 
+let rebuild_cons env nb_args relname args crossed_types rt = 
 (*   observennl  (str "rebuild_cons : rt := "++ pr_rawconstr rt ++  *)
 (* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
   let res = 
-    rebuild_cons nb_args relname args crossed_types 0 rt 
+    rebuild_cons env nb_args relname args crossed_types 0 rt 
   in
 (*   observe (str " leads to "++ pr_rawconstr (fst res)); *)
   res
@@ -1103,6 +1215,35 @@ let do_build_inductive
       (Global.env ())
   in      
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in 
+  let env_with_graphs = 
+    let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
+      let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list  = 
+	funargs
+      in 
+      List.fold_right
+	(fun (n,t,is_defined) acc -> 
+	   if is_defined
+	   then 
+	     Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t,
+			      acc)
+	   else
+	     Topconstr.CProdN
+	       (dummy_loc,
+		[[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t],
+		acc
+	       )
+	)
+	rel_first_args
+	(rebuild_return_type returned_types.(i))
+    in
+    (* We need to lift back our work topconstr but only with all information 
+       We mimick a Set Printing All. 
+       Then save the graphs and reset Printing options to their primitive values 
+    *)
+    let rel_arities = Array.mapi rel_arity funsargs in
+    Util.array_fold_left2 (fun env rel_name rel_ar -> 
+			     Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities
+  in
   (* and of the real constructors*)
   let constr i res = 
     List.map 
@@ -1111,7 +1252,7 @@ let do_build_inductive
 	 let nb_args = List.length funsargs.(i) in 
 	 (*  with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
 	 fst (
-	   rebuild_cons nb_args relnames.(i)
+	   rebuild_cons env_with_graphs nb_args relnames.(i)
 	     []
 	     []
 	     rt