From 133a2143413a723d1d4e3dead5ffa8458f61afa8 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 24 Oct 2013 21:29:35 +0000
Subject: inductive.ml : get rid of some obvious (Lazy.force (lazy t))

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16935 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/inductive.ml | 12 +++++-------
 kernel/inductive.ml  | 12 +++++-------
 2 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 4dcf3d3f19..ad7c472d99 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -400,10 +400,10 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
-let spec_of_tree t = lazy
-  (if eq_wf_paths (Lazy.force t) mk_norec
-   then Not_subterm
-   else Subterm(Strict,Lazy.force t))
+let spec_of_tree t =
+  if eq_wf_paths t mk_norec
+  then Not_subterm
+  else Subterm (Strict, t)
 
 let subterm_spec_glb =
   let glb2 s1 s2 =
@@ -525,9 +525,7 @@ let branches_specif renv c_spec ci =
 		Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) ->
 		  let vra = Array.of_list (dest_subterms t).(i) in
 		  assert (nca = Array.length vra);
-		  Array.map
-		    (fun t -> Lazy.force (spec_of_tree (lazy t)))
-		    vra
+		  Array.map spec_of_tree vra
 	      | Dead_code -> Array.make nca Dead_code
 	      | _ -> Array.make nca Not_subterm) in
 	 List.init nca (fun j -> lazy (Lazy.force lvra).(j)))
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e3e636e4aa..3c7103ac53 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -421,10 +421,10 @@ type subterm_spec =
 
 let eq_wf_paths = Rtree.equal Declareops.eq_recarg
 
-let spec_of_tree t = lazy
-  (if eq_wf_paths (Lazy.force t) mk_norec
-   then Not_subterm
-   else Subterm(Strict,Lazy.force t))
+let spec_of_tree t =
+  if eq_wf_paths t mk_norec
+  then Not_subterm
+  else Subterm (Strict, t)
 
 let subterm_spec_glb =
   let glb2 s1 s2 = 
@@ -526,9 +526,7 @@ let branches_specif renv c_spec ci =
 		Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) ->
 		  let vra = Array.of_list (dest_subterms t).(i) in
 		  assert (Int.equal nca (Array.length vra));
-		  Array.map
-		    (fun t -> Lazy.force (spec_of_tree (lazy t)))
-		    vra
+		  Array.map spec_of_tree vra
 	      | Dead_code -> Array.make nca Dead_code
 	      | _ -> Array.make nca Not_subterm) in
 	 List.init nca (fun j -> lazy (Lazy.force lvra).(j)))
-- 
cgit v1.2.3