Use typing informations while defining graphs for Function.

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

3 files changed, 233 insertions, 150 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index a60a4f4fc..ba60f49ed 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -9,11 +9,11 @@ open Util
 open Rawtermops
 
 let observe strm =  
-  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  && false 
+  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  
   then Pp.msgnl strm 
   else ()
 let observennl strm =  
-  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  &&false 
+  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  
   then Pp.msg strm 
   else ()
 
@@ -295,7 +295,7 @@ let pr_name = function
 (**********************************************************************)		
 
 (* [build_constructors_of_type] construct the array of pattern of its inductive argument*)	  
-let build_constructors_of_type msg ind' argl = 
+let build_constructors_of_type ind' argl = 
   let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
   let npar = mib.Declarations.mind_nparams in
   Array.mapi (fun i _ ->
@@ -324,15 +324,6 @@ let build_constructors_of_type msg ind' argl =
 	     )
     ind.Declarations.mind_consnames
 
-(* construction of the branches from an inductive*)    
-let find_constructors_of_raw_type msg t argl : Rawterm.cases_pattern array  =
-  let ind,args = raw_decompose_app t in
-  match ind with
-    | RRef(_,IndRef ind')  ->
-	build_constructors_of_type msg ind' argl
-    | _ -> error msg
-	
-
 (* [find_type_of] very naive attempts to discover the type of an if or a letin *)
 let rec find_type_of nb b = 
   let f,_ = raw_decompose_app b in 
@@ -371,6 +362,60 @@ let rec find_type_of nb b =
 (* Main functions *)
 (******************)
 
+
+
+let raw_push_named (na,raw_value,raw_typ) env = 
+  match na with 
+    | Anonymous -> env 
+    | Name id -> 
+	let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in 
+	let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in 
+	Environ.push_named (id,value,typ) env
+
+
+let add_pat_variables pat typ env : Environ.env = 
+  let rec add_pat_variables env pat typ  : Environ.env = 
+    observe (str "new rel env := " ++ Printer.pr_rel_context_of env);
+
+    match pat with 
+      | PatVar(_,na) -> Environ.push_rel (na,None,typ) env 
+      | PatCstr(_,c,patl,na) -> 
+	  let Inductiveops.IndType(indf,indargs) = 
+	    try Inductiveops.find_rectype env Evd.empty typ
+	    with Not_found -> assert false 
+	  in
+	  let constructors = Inductiveops.get_constructors env indf in 
+	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in 
+	  let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in 
+	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) 
+  in
+  let new_env = add_pat_variables  env pat typ in 
+  let res =
+    fst (
+      Sign.fold_rel_context
+	(fun (na,v,t) (env,ctxt) ->
+	 match na with
+	   | Anonymous -> assert false
+	   | Name id ->
+	       let new_t =  substl ctxt t in
+	       let new_v = option_map (substl ctxt) v in
+	       observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
+			  str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
+			  str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
+			  option_fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
+			  option_fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
+		       );
+	       (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
+      )
+	(Environ.rel_context new_env)
+	~init:(env,[])
+    )
+  in
+  observe (str "new var env := " ++ Printer.pr_named_context_of res);
+  res
+
+
+
 (* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) 
    of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the 
    corresponding graphs. 
@@ -403,8 +448,8 @@ let rec find_type_of nb b =
 *)
 
 
-let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return = 
-(*   Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *)
+let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return = 
+  observe (str " Entering : " ++ Printer.pr_rawconstr rt);
   match rt with 
     | RRef _ | RVar _ | REvar _ | RPatVar _     | RSort _  | RHole _  -> 
 	(* do nothing (except changing type of course) *)
@@ -414,8 +459,8 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 	let args_res : (rawconstr list) build_entry_return =
 	  List.fold_right (* create the arguments lists of constructors and combine them *)
 	    (fun arg ctxt_argsl ->
-	       let arg_res = build_entry_lc funnames ctxt_argsl.to_avoid arg in
-	       combine_results combine_args  arg_res ctxt_argsl
+	       let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
+	       combine_results combine_args arg_res ctxt_argsl
 	    )
 	    args
 	    (mk_result [] [] avoid)
@@ -430,6 +475,9 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 		   a pseudo value "v1 ... vn". 
 		   The "value" of this branch is then simply [res]
 		*)
+		let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in 
+		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in 
+		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
 		let res = fresh_id args_res.to_avoid "res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkRVar res in 
@@ -437,7 +485,7 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 		  List.map 
 		    (fun arg_res -> 
 		       let new_hyps = 
-			 [Prod (Name res),mkRHole ();
+			 [Prod (Name res),res_raw_type;
 			  Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
 		       in
 		       {context =  arg_res.context@new_hyps; value = res_rt } 
@@ -481,6 +529,7 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 		    | _ -> n,b,avoid
 		in
 		build_entry_lc 
+		  env
 		  funnames 
 		  avoid
 		  (mkRLetIn(new_n,t,mkRApp(new_b,args)))
@@ -489,7 +538,7 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 		   we first compute the result from the case and 
 		   then combine each of them with each of args one
 		*)
-		let f_res = build_entry_lc funnames  args_res.to_avoid f in
+		let f_res = build_entry_lc env funnames args_res.to_avoid f in
 		combine_results combine_app f_res  args_res
 	    | RDynamic _ ->error "Not handled RDynamic" 
 	    | RCast(_,b,_,_) -> 
@@ -498,7 +547,7 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 
 		   WARNING: We need to restart since [b] itself should be an application term
 		*)
-		build_entry_lc funnames  avoid (mkRApp(b,args))
+		build_entry_lc env funnames avoid (mkRApp(b,args))
 	    | RRec _ -> error "Not handled RRec"
 	    | RProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *) 
@@ -509,13 +558,14 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 	   then the one corresponding to the type 
 	   and combine the two result
 	*)
-	let b_res = build_entry_lc funnames avoid b in
-	let t_res = build_entry_lc funnames avoid t  in
+	let t_res = build_entry_lc env funnames avoid t  in
 	let new_n = 
 	  match n with 
 	    | Name _ -> n 
 	    | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
 	in
+	let new_env = raw_push_named (new_n,None,t) env in
+	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_lam new_n) t_res b_res
     | RProd(_,n,t,b) ->
 	(* we first compute the list of constructor 
@@ -523,106 +573,88 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 	   then the one corresponding to the type 
 	   and combine the two result
 	*)
-	let b_res = build_entry_lc funnames avoid b in
-	let t_res = build_entry_lc funnames avoid t in
+	let t_res = build_entry_lc env funnames avoid t in
+	let new_env = raw_push_named (n,None,t) env in
+	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_prod n) t_res b_res
-    | RLetIn(_,n,t,b) ->
+    | RLetIn(_,n,v,b) ->
 	(* we first compute the list of constructor 
 	   corresponding to the body of the function, 
 	   then the one corresponding to the value [t] 
 	   and combine the two result
 	*)
-	let b_res = build_entry_lc funnames avoid b in
-	let t_res = build_entry_lc funnames avoid t in
-	combine_results (combine_letin n) t_res b_res
+	let v_res = build_entry_lc env funnames avoid v in
+	let v_as_constr = Pretyping.Default.understand Evd.empty env v in 
+	let v_type = Typing.type_of env Evd.empty v_as_constr in 
+	let new_env = 
+	  match n with
+	      Anonymous -> env
+	    | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env 
+	in
+	let b_res = build_entry_lc new_env funnames avoid b in
+	combine_results (combine_letin n) v_res b_res
     | RCases(_,_,el,brl) -> 
 	(* we create the discrimination function 
 	   and treat the case itself 
 	*)
 	let make_discr = make_discr_match brl in 
-	build_entry_lc_from_case funnames make_discr el brl avoid
+	build_entry_lc_from_case env funnames make_discr el brl avoid
     | RIf(_,b,(na,e_option),lhs,rhs) -> 
-	(* Same as RCases but we need to compute the branches *)
-	begin
-	  match b with 
-	    | RCast(_,b,_,t) -> 
-		let msg = "If construction must be used with cast" in 
-		let case_pat = find_constructors_of_raw_type msg t [] in 
-		assert (Array.length case_pat = 2);
-		let brl = 
-		  list_map_i
-		    (fun i x -> (dummy_loc,[],[case_pat.(i)],x)) 
-		    0
-		    [lhs;rhs]
-		in 
-		let match_expr =
-		  mkRCases(None,[(b,(Anonymous,None))],brl)
-		in
-(* 		Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
-		build_entry_lc funnames avoid match_expr
-	    | _ ->  
-		try 
-		  let ind = find_type_of 2 b in 
-		  let case_pat = build_constructors_of_type (str "") ind [] in 
-		  let brl = 
-		  list_map_i
-		    (fun i x -> (dummy_loc,[],[case_pat.(i)],x)) 
-		    0
-		    [lhs;rhs]
-		in 
-		let match_expr =
-		  mkRCases(None,[(b,(Anonymous,None))],brl)
-		in
-		(* 		Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
-		build_entry_lc funnames avoid match_expr
-		with Invalid_argument s -> 
-		  let msg = "If construction must be used with cast : "^ s in 
-		  error msg
-		  
-	end
+	let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+	let b_typ = Typing.type_of env Evd.empty b_as_constr in 
+	let (ind,_) =  
+	  try Inductiveops.find_inductive env Evd.empty b_typ 
+	  with Not_found -> 
+	    errorlabstrm "" (str "Cannot find the inductive associated to " ++ 
+			       Printer.pr_rawconstr b ++ str " in " ++
+			       Printer.pr_rawconstr rt ++ str ". try again with a cast")
+	in
+	let case_pats = build_constructors_of_type ind [] in 
+	assert (Array.length case_pats = 2);
+	let brl =
+	  list_map_i
+	    (fun i x -> (dummy_loc,[],[case_pats.(i)],x))
+	    0
+	    [lhs;rhs]
+	in
+	let match_expr =
+	  mkRCases(None,[(b,(Anonymous,None))],brl)
+	in
+	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
+	build_entry_lc env funnames avoid match_expr
     | RLetTuple(_,nal,_,b,e) ->  
-	begin 
-	(* Same as RCases but we need to compute the branches *)
-	  let nal_as_rawconstr = 
-	    List.map 
-	      (function 
-		   Name id -> mkRVar id 
+	begin
+	  let nal_as_rawconstr =
+	    List.map
+	      (function
+		   Name id -> mkRVar id
 		 | Anonymous -> mkRHole ()
 	      )
-	      nal 
+	      nal
 	  in
-	  match b with 
-	    | RCast(_,b,_,t) -> 
-		let case_pat = 
-		  find_constructors_of_raw_type 
-		    "LetTuple construction must be used with cast" t nal_as_rawconstr in
-		assert (Array.length case_pat = 1);
-		let br = 
-		  (dummy_loc,[],[case_pat.(0)],e) 
-		in
-		let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in 
-		build_entry_lc funnames avoid match_expr
-	    | _ -> 
-		try 
-		  let ind = find_type_of 1 b in 
-		  let case_pat = 
-		    build_constructors_of_type 
-		      (str "LetTuple construction must be used with cast") ind nal_as_rawconstr in 
-		  let br = 
-		    (dummy_loc,[],[case_pat.(0)],e) 
-		  in
-		  let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in 
-		  build_entry_lc funnames avoid match_expr
-		with Invalid_argument s -> 
-		  let msg = "LetTuple construction must be used with cast : "^ s in 
-		  error msg
-		
+	  let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+	  let b_typ = Typing.type_of env Evd.empty b_as_constr in 
+	  let (ind,_) = 
+	    try Inductiveops.find_inductive env Evd.empty b_typ 
+	    with Not_found -> 
+	      errorlabstrm "" (str "Cannot find the inductive associated to " ++ 
+				 Printer.pr_rawconstr b ++ str " in " ++
+				 Printer.pr_rawconstr rt ++ str ". try again with a cast")
+	  in
+	  let case_pats = build_constructors_of_type ind nal_as_rawconstr in 
+	  assert (Array.length case_pats = 1);
+	  let br =
+	    (dummy_loc,[],[case_pats.(0)],e)
+	  in
+	  let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
+	  build_entry_lc env funnames avoid match_expr
+
 	end
     | RRec _ -> error "Not handled RRec"
     | RCast(_,b,_,_) -> 
-	build_entry_lc funnames  avoid b
+	build_entry_lc env funnames  avoid b
     | RDynamic _ -> error "Not handled RDynamic"
-and build_entry_lc_from_case funname make_discr
+and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuple)
     (brl:Rawterm.cases_clauses) avoid : 
     rawconstr build_entry_return = 
@@ -640,15 +672,26 @@ and build_entry_lc_from_case funname make_discr
 	let case_resl = 
 	    List.fold_right
 	    (fun (case_arg,_) ctxt_argsl ->
-	       let arg_res = build_entry_lc funname avoid case_arg  in
+	       let arg_res = build_entry_lc env funname avoid case_arg  in
 	       combine_results combine_args arg_res ctxt_argsl
 	    )
 	    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
 	let results =
 	  List.map 
-	    (build_entry_lc_from_case_term funname (make_discr (List.map fst el)) []  brl case_resl.to_avoid) 
+	    (build_entry_lc_from_case_term
+	       env types
+	       funname (make_discr (List.map fst el))
+	       []  brl 
+	       case_resl.to_avoid) 
 	    case_resl.result 
 	in 
 	{ 
@@ -657,7 +700,7 @@ and build_entry_lc_from_case funname make_discr
 	    List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
 	} 
 
-and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avoid
+and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
     matched_expr =
   match brl with
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
@@ -668,18 +711,26 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
 	(* building a list of precondition stating that we are not in this branch 
 	   (will be used in the following recursive calls)
 	*)
+	let new_env = List.fold_right2 add_pat_variables patl types env in 
 	let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list = 
-	  List.map 
-	    (fun pat -> 
+	  List.map2
+	    (fun pat typ -> 
 	       fun avoid pat'_as_term -> 
 		 let renamed_pat,_,_ = alpha_pat avoid pat in
 		 let pat_ids = get_pattern_id renamed_pat  in 
-		 List.fold_right 
-		   (fun id acc -> mkRProd (Name id,mkRHole (),acc))
+		 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))
 	    )
 	    patl
+	    types
 	in
 	(* Checking if we can be in this branch 
 	   (will be used in the following recursive calls)
@@ -695,6 +746,8 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
 	*)
 	let brl'_res =
 	  build_entry_lc_from_case_term
+	    env 
+	    types
 	    funname
 	    make_discr
 	    ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
@@ -712,22 +765,30 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
       	let those_pattern_preconds =
 	  (List.flatten
 	    (
-	    List.map2
-	      (fun pat e ->
+	      list_map3
+	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in 
+		 let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right 
 		   (fun id  acc -> 
 		      if Idset.mem id this_pat_ids 
-		      then (Prod (Name id),mkRHole ())::acc
+		      then (Prod (Name id),
+		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in 
+		      let raw_typ_of_id = 
+			Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id
+		      in
+		      raw_typ_of_id
+			   )::acc
 		      else acc
 			
 		   )
 		   idl
-		   [(Prod Anonymous,raw_make_eq pat_as_term e)]
+		   [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)]
 	      )
 	      patl
 	      matched_expr.value
+	      types
 	  )
 	  )
 	  @
@@ -738,13 +799,13 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
 			     List.for_all (fun x -> x) unif) patterns_to_prevent
 	   then 
 	     let i = List.length patterns_to_prevent in 
-	     [(Prod Anonymous,make_discr  i  )]
+	     [(Prod Anonymous,make_discr i  )]
 	   else 
 	     []
 	  )
 	in
 	(* We compute the result of the value returned by the branch*)
-	let return_res = build_entry_lc funname new_avoid return in
+	let return_res = build_entry_lc new_env funname new_avoid return in
 	(* and combine it with the preconds computed for this branch *)
 	let this_branch_res =
 	  List.map
@@ -796,7 +857,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 			assert false 
 		end
 	    | RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt]) 
-		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  
+		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 = 
@@ -997,14 +1058,34 @@ let build_inductive
   let relnames = Array.map mk_rel_id funnames in
   let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in 
   (* Construction of the pseudo constructors *)
-  let resa = Array.map (build_entry_lc funnames_as_set []) rta in 
+  let env = 
+    Array.fold_right 
+      (fun id env -> 
+	 Environ.push_named (id,None,Typing.type_of env Evd.empty (Tacinterp.constr_of_id env id))  env
+      )
+      funnames 
+      (Global.env ())
+  in      
+  let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in 
   (* and of the real constructors*)
   let constr i res = 
     List.map 
       (function result (* (args',concl') *) -> 
 	 let rt = compose_raw_context result.context result.value in 
 	 let nb_args = List.length funsargs.(i) in 
-(* 	 Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+(* 	   let old_implicit_args = Impargs.is_implicit_args () *)
+(* 	   and old_strict_implicit_args =  Impargs.is_strict_implicit_args () *)
+(* 	   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in *)
+(* 	   let old_rawprint = !Options.raw_print in  *)
+(* 	   Options.raw_print := true; *)
+(* 	   Impargs.make_implicit_args false; *)
+(* 	   Impargs.make_strict_implicit_args false; *)
+(* 	   Impargs.make_contextual_implicit_args false; *)
+(* 	   Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+(* 	   Impargs.make_implicit_args old_implicit_args; *)
+(* 	   Impargs.make_strict_implicit_args old_strict_implicit_args; *)
+(* 	   Impargs.make_contextual_implicit_args old_contextual_implicit_args; *)
+(* 	   Options.raw_print := old_rawprint; *)
 	 fst (
 	   rebuild_cons nb_args relnames.(i)
 	     []
@@ -1096,26 +1177,26 @@ let build_inductive
   in
   let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
   let rel_inds = Array.to_list ext_rel_constructors in 
-  let _ = 
-    observe (
-      str "Inductive" ++ spc () ++
-	prlist_with_sep 
-	(fun () -> fnl ()++spc () ++ str "with" ++ spc ()) 
-	(function ((_,id),_,params,ar,constr) -> 
-	   Ppconstr.pr_id id ++ spc () ++ 
-	     Ppconstr.pr_binders params ++ spc () ++
-	     str ":" ++ spc () ++ 
-	     Ppconstr.pr_lconstr_expr ar ++ spc () ++ 
-	     prlist_with_sep 
-	     (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ())
-	     (function (_,((_,id),t)) -> 
-		Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++
-		  Ppconstr.pr_lconstr_expr t)
-	     constr
-	)
-	rel_inds
-    )
-  in
+(*   let _ =  *)
+(*   Pp.msgnl  (\* observe *\) ( *)
+(*       str "Inductive" ++ spc () ++ *)
+(* 	prlist_with_sep  *)
+(* 	(fun () -> fnl ()++spc () ++ str "with" ++ spc ())  *)
+(* 	(function ((_,id),_,params,ar,constr) ->  *)
+(* 	   Ppconstr.pr_id id ++ spc () ++  *)
+(* 	     Ppconstr.pr_binders params ++ spc () ++ *)
+(* 	     str ":" ++ spc () ++  *)
+(* 	     Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *)
+(* 	     prlist_with_sep  *)
+(* 	     (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *)
+(* 	     (function (_,((_,id),t)) ->  *)
+(* 		Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *)
+(* 		  Ppconstr.pr_lconstr_expr t) *)
+(* 	     constr *)
+(* 	) *)
+(* 	rel_inds *)
+(*     ) *)
+(*   in *)
   let old_implicit_args = Impargs.is_implicit_args ()
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 96b0e1eb7..204249f1d 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
 let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
 let mkRSort s = RSort(dummy_loc,s)
 let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
-
+let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t)
 
 (*
   Some basic functions to decompose rawconstrs
@@ -49,8 +49,8 @@ let raw_decompose_app =
 
 
 (* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) 
-let raw_make_eq t1 t2  = 
-  mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[mkRHole ();t2;t1])
+let raw_make_eq ?(typ= mkRHole ()) t1 t2  = 
+  mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1])
 
 (* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) 
 let raw_make_neq t1 t2 = 
@@ -386,30 +386,32 @@ let is_free_in id =
       
 
 
-let rec pattern_to_term  = function 
+let rec pattern_to_term  = function
   | PatVar(loc,Anonymous) -> assert false
-  | PatVar(loc,Name id) -> 
+  | PatVar(loc,Name id) ->
 	mkRVar id
-  | PatCstr(loc,constr,patternl,_) -> 
-      let cst_narg = 
+  | PatCstr(loc,constr,patternl,_) ->
+      let cst_narg =
 	Inductiveops.mis_constructor_nargs_env
 	  (Global.env ())
 	  constr
       in
-      let implicit_args =  
-	Array.to_list 
-	  (Array.init 
+      let implicit_args =
+	Array.to_list
+	  (Array.init
 	     (cst_narg - List.length patternl)
 	     (fun _ -> mkRHole ())
 	  )
       in
-      let patl_as_term = 
+      let patl_as_term =
 	List.map pattern_to_term patternl
       in
       mkRApp(mkRRef(Libnames.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
 
+  
+
 let replace_var_by_term x_id term = 
   let rec replace_var_by_pattern rt = 
     match rt with 
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 4df239e32..aa3554850 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -25,7 +25,7 @@ val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
 val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr
 val mkRSort : rawsort -> rawconstr 
 val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
-
+val mkRCast : rawconstr* rawconstr -> rawconstr 
 (*
   Some basic functions to decompose rawconstrs
   These are analogous to the ones constrs
@@ -36,7 +36,7 @@ val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
 
 
 (* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) 
-val  raw_make_eq : rawconstr -> rawconstr -> rawconstr
+val  raw_make_eq : ?typ:rawconstr -> rawconstr -> rawconstr -> rawconstr
 (* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) 
 val  raw_make_neq : rawconstr -> rawconstr -> rawconstr
 (* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)