Second step of integration of Program:

- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.

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

3 files changed, 18 insertions, 19 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6a58888743..a7298095ea 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -368,8 +368,8 @@ let raw_push_named (na,raw_value,raw_typ) env =
   match na with
     | Anonymous -> env
     | Name id ->
-	let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in
-	let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in
+	let value = Option.map (Pretyping.understand Evd.empty env) raw_value in
+	let typ = Pretyping.understand_type Evd.empty env raw_typ in
 	Environ.push_named (id,value,typ) env
 
 
@@ -521,7 +521,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr 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_as_constr = Pretyping.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
@@ -629,7 +629,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	   and combine the two result
 	*)
 	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_as_constr = Pretyping.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
@@ -645,7 +645,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let make_discr = make_discr_match brl in
 	build_entry_lc_from_case env funnames make_discr el brl avoid
     | GIf(_,b,(na,e_option),lhs,rhs) ->
-	let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+	let b_as_constr = Pretyping.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
@@ -677,7 +677,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	      )
 	      nal
 	  in
-	  let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+	  let b_as_constr = Pretyping.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
@@ -724,7 +724,7 @@ and build_entry_lc_from_case env funname make_discr
 	in
 	let types =
 	  List.map (fun (case_arg,_) ->
-		      let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in
+		      let case_arg_as_constr = Pretyping.understand Evd.empty env case_arg in
 		      Typing.type_of env Evd.empty case_arg_as_constr
 		   ) el
 	in
@@ -928,7 +928,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			let new_t =
 			  mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
 			in
-			let t' = Pretyping.Default.understand Evd.empty env new_t in
+			let t' = Pretyping.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
@@ -948,7 +948,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  try
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
 		    let t' =
-		      try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue
+		      try Pretyping.understand Evd.empty env t with _ -> raise Continue
 		    in
 		    let is_in_b = is_free_in id b in
 		    let _keep_eq =
@@ -970,7 +970,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
 		    let jmeq = Libnames.IndRef (destInd (jmeq ())) in
-		    let ty' = Pretyping.Default.understand Evd.empty env ty in
+		    let ty' = Pretyping.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
@@ -992,7 +992,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt])
 		    in
 		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
-		    let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in
+		    let eq'_as_constr = Pretyping.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
@@ -1040,7 +1040,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     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
+		      let t' = Pretyping.understand Evd.empty env eq' in
 		      Environ.push_rel (n,None,t') env
 		    in
 		    let new_b,id_to_exclude =
@@ -1078,7 +1078,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  else raise Continue
 	      with Continue -> 
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t' = Pretyping.Default.understand Evd.empty env t in
+		let t' = Pretyping.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 new_env
@@ -1094,7 +1094,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      end
 	    | _ ->
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t' = Pretyping.Default.understand Evd.empty env t in
+		let t' = Pretyping.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 new_env
@@ -1113,7 +1113,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  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_glob_constr rt);
-	  let t' = Pretyping.Default.understand Evd.empty env t in
+	  let t' = Pretyping.understand Evd.empty env t in
 	  match n with
 	    | Name id ->
 		let new_env = Environ.push_rel (n,None,t') env in
@@ -1135,7 +1135,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     | GLetIn(_,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 t' = Pretyping.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 =
@@ -1160,7 +1160,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      args (crossed_types)
 	      depth t
 	  in
-	  let t' = Pretyping.Default.understand Evd.empty env new_t in
+	  let t' = Pretyping.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 new_env
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 3b3f3057b6..3ea9c3d3e7 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -49,7 +49,7 @@ let rec substitterm prof t by_t in_u =
 
 let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl
 
-let understand = Pretyping.Default.understand Evd.empty (Global.env())
+let understand = Pretyping.understand Evd.empty (Global.env())
 
 (** Operations on names and identifiers *)
 let id_of_name = function
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c37de6e4a6..0f92378d68 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -36,7 +36,6 @@ open Pfedit
 open Topconstr
 open Glob_term
 open Pretyping
-open Pretyping.Default
 open Safe_typing
 open Constrintern
 open Hiddentac