kernel/declarations becomes a pure mli

 - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
 - the functions that were in declarations.ml (mostly substitution utilities
   and hashcons) are now in kernel/declareops.ml

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

3 files changed, 17 insertions, 10 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5aee45dccc..ae60259e9f 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -136,7 +136,7 @@ let check_arity env cb =
 let check_fix env cb i =
   match cb.const_body with
     | Def lbody ->
-	(match kind_of_term (Declarations.force lbody) with
+	(match kind_of_term (Lazyconstr.force lbody) with
 	  | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
 	  | _ -> raise Impossible)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c8f3765657..035f8e3bb2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -11,6 +11,7 @@ open Util
 open Names
 open Term
 open Declarations
+open Declareops
 open Environ
 open Reduction
 open Reductionops
@@ -277,7 +278,7 @@ let rec extract_type env db j c args =
 		  | Undef _ | OpaqueDef _ -> mlt
 		  | Def _ when is_custom r -> mlt
 		  | Def lbody ->
-		      let newc = applist (Declarations.force lbody, args) in
+		      let newc = applist (Lazyconstr.force lbody, args) in
 		      let mlt' = extract_type env db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
 		      (* reduction, so [mlt] and [mlt'] might be different: *)
@@ -291,7 +292,7 @@ let rec extract_type env db j c args =
 		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
 		  | Def lbody ->
 		      (* We try to reduce. *)
-		      let newc = applist (Declarations.force lbody, args) in
+		      let newc = applist (Lazyconstr.force lbody, args) in
 		      extract_type env db j newc []))
     | Ind (kn,i) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
@@ -515,7 +516,7 @@ and mlt_env env r = match r with
 	   | Def l_body ->
 	       (match flag_of_type env typ with
 		  | Info,TypeScheme ->
-		      let body = Declarations.force l_body in
+		      let body = Lazyconstr.force l_body in
 		      let s,vl = type_sign_vl env typ in
 		      let db = db_from_sign s in
 		      let t = extract_type_scheme env db body (List.length s)
@@ -986,17 +987,21 @@ let extract_constant env kn cb =
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c -> mk_typ (force c)
+	  | Def c -> mk_typ (Lazyconstr.force c)
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then mk_typ (force_opaque c) else mk_typ_ax ())
+	    if access_opaque () then
+              mk_typ (Lazyconstr.force_opaque c)
+            else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
-	  | Def c -> mk_def (force c)
+	  | Def c -> mk_def (Lazyconstr.force c)
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then mk_def (force_opaque c) else mk_ax ())
+	    if access_opaque () then
+              mk_def (Lazyconstr.force_opaque c)
+            else mk_ax ())
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
@@ -1010,7 +1015,8 @@ let extract_constant_spec env kn cb =
 	  | Undef _ | OpaqueDef _ -> Stype (r, vl, None)
 	  | Def body ->
 	      let db = db_from_sign s in
-	      let t = extract_type_scheme env db (force body) (List.length s)
+              let body = Lazyconstr.force body in
+	      let t = extract_type_scheme env db body (List.length s)
 	      in Stype (r, vl, Some t))
     | (Info, Default) ->
 	let t = snd (record_constant_type env kn (Some typ)) in
@@ -1023,7 +1029,7 @@ let extract_with_type env cb =
 	let s,vl = type_sign_vl env typ in
 	let db = db_from_sign s in
 	let c = match cb.const_body with
-	  | Def body -> force body
+	  | Def body -> Lazyconstr.force body
 	  (* A "with Definition ..." is necessarily transparent *)
 	  | Undef _ | OpaqueDef _ -> assert false
 	in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 8ecd8cd7c4..4407c67986 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1289,6 +1289,7 @@ let is_not_strict t =
 *)
 
 open Declarations
+open Declareops
 
 let inline_test r t =
   if not (auto_inline ()) then false