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

5 files changed, 12 insertions, 8 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 450b3ef405..3c92bb5bd6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -5,6 +5,7 @@ open Term
 open Namegen
 open Names
 open Declarations
+open Declareops
 open Pp
 open Hiddentac
 open Tacmach
@@ -947,7 +948,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let f_def = Global.lookup_constant (destConst f) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
   let f_body =
-    force (Option.get (body_of_constant f_def))
+    Lazyconstr.force (Option.get (body_of_constant f_def))
   in
   let params,f_body_with_params = decompose_lam_n nb_params f_body in
   let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -1065,7 +1066,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
     let get_body const =
       match body_of_constant (Global.lookup_constant const) with
 	| Some b ->
-	     let body = force b in
+	     let body = Lazyconstr.force b in
 	     Tacred.cbv_norm_flags
 	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 	       (Global.env ())
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9916ed95a9..debf96345a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -5,6 +5,7 @@ open Term
 open Namegen
 open Names
 open Declarations
+open Declareops
 open Pp
 open Entries
 open Tactics
@@ -404,7 +405,7 @@ let get_funs_constant mp dp =
     let find_constant_body const =
       match body_of_constant (Global.lookup_constant const) with
 	| Some b ->
-	    let body = force b in
+	    let body = Lazyconstr.force b in
 	    let body = Tacred.cbv_norm_flags
 	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 	      (Global.env ())
@@ -539,7 +540,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
     let finfos = find_Function_infos this_block_funs.(0) in
     try
       let equation =  Option.get finfos.equation_lemma in
-      Declarations.is_opaque (Global.lookup_constant equation)
+      Declareops.is_opaque (Global.lookup_constant equation)
     with Option.IsNone -> (* non recursive definition *)
       false
   in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 99bf66d1f7..fd4e23de7a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -8,6 +8,7 @@ open Libnames
 open Globnames
 open Glob_term
 open Declarations
+open Declareops
 open Misctypes
 open Decl_kinds
 
@@ -770,7 +771,7 @@ let make_graph (f_ref:global_reference) =
      | None -> error "Cannot build a graph over an axiom !"
      | Some b ->
 	 let env = Global.env () in
-	 let body = (force b) in
+	 let body = Lazyconstr.force b in
 	 let extern_body,extern_type =
 	   with_full_print
 	     (fun () ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 92d2fe680f..9879f08a00 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -121,8 +121,8 @@ let const_of_id id =
 let def_of_const t =
    match (Term.kind_of_term t) with
     Term.Const sp ->
-      (try (match Declarations.body_of_constant (Global.lookup_constant sp) with
-             | Some c -> Declarations.force c
+      (try (match Declareops.body_of_constant (Global.lookup_constant sp) with
+             | Some c -> Lazyconstr.force c
 	     | _ -> assert false)
        with _ -> assert false)
     |_ -> assert false
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d5e1ee53ab..bea019259e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -10,6 +10,7 @@ open Term
 open Namegen
 open Environ
 open Declarations
+open Declareops
 open Entries
 open Pp
 open Names
@@ -68,7 +69,7 @@ let def_of_const t =
    match (kind_of_term t) with
     Const sp ->
       (try (match body_of_constant (Global.lookup_constant sp) with
-             | Some c -> Declarations.force c
+             | Some c -> Lazyconstr.force c
 	     | _ -> assert false)
        with _ ->
 	 anomaly (str "Cannot find definition of constant " ++