6 files changed, 7 insertions, 12 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ef4dca26d..74d719438 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -940,8 +940,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 (*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
   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 =
-    Lazyconstr.force (Option.get (body_of_constant f_def))
+  let f_body = 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
@@ -1058,8 +1057,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
     in
     let get_body const =
       match body_of_constant (Global.lookup_constant const) with
-	| Some b ->
-	     let body = Lazyconstr.force b in
+	| Some body ->
 	     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 09637d273..50a4703f6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -403,8 +403,7 @@ let get_funs_constant mp dp =
   function const ->
     let find_constant_body const =
       match body_of_constant (Global.lookup_constant const) with
-	| Some b ->
-	    let body = Lazyconstr.force b in
+	| Some body ->
 	    let body = Tacred.cbv_norm_flags
 	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 	      (Global.env ())
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f0f76860a..609e2916d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -766,9 +766,8 @@ let make_graph (f_ref:global_reference) =
   Dumpglob.pause ();
   (match body_of_constant c_body with
      | None -> error "Cannot build a graph over an axiom !"
-     | Some b ->
+     | Some body ->
 	 let env = Global.env () 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 4d1cefe5a..1e8f4afdf 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -116,7 +116,7 @@ let def_of_const t =
    match (Term.kind_of_term t) with
     Term.Const sp ->
       (try (match Declareops.body_of_constant (Global.lookup_constant sp) with
-             | Some c -> Lazyconstr.force c
+             | Some c -> c
 	     | _ -> assert false)
        with Not_found -> assert false)
     |_ -> assert false
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 597233d01..a8ffd51ef 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -69,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 -> Lazyconstr.force c
+             | Some c -> c
 	     | _ -> raise Not_found)
        with Not_found ->
 	 anomaly (str "Cannot find definition of constant " ++
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index a34d4a682..ddc4725c3 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -229,8 +229,7 @@ let mk_constant_obj id bo ty variables hyps =
       Acic.Constant (Names.Id.to_string id,None,ty,params)
    | Some c ->
       Acic.Constant
-       (Names.Id.to_string id, Some (Unshare.unshare (Lazyconstr.force c)),
-         ty,params)
+       (Names.Id.to_string id, Some (Unshare.unshare c), ty,params)
 ;;
 
 let mk_inductive_obj sp mib packs variables nparams hyps finite =