Cleanup code for looking up projection bodies.

3 files changed, 17 insertions, 46 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index 6f19fc59f0..8791462845 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -799,13 +799,11 @@ let rec knh info m stk =
     | FCast(t,_,_) -> knh info t stk
 
     | FProj (p,c) ->
-        (* if red_set info.i_flags (fCONST p) then *)
-          (match try Some (lookup_projection p (info.i_env)) with Not_found -> None with
-	  | None -> (m, stk)
-	  | Some pb ->
-	     knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
-			 :: zupdate m stk))
-	(* else (m,stk) *)
+      if red_set info.i_flags (fCONST p) then
+        (let pb = lookup_projection p (info.i_env) in
+	   knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
+		       :: zupdate m stk))
+      else (m,stk)
 
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|
diff --git a/checker/reduction.ml b/checker/reduction.ml
index b8677f5aaa..0886ab7485 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -216,13 +216,9 @@ let oracle_order fl1 fl2 =
     | _ -> false
 
 let unfold_projection infos p c =
-  (* if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then *)
-    (match try Some (lookup_projection p (infos_env infos)) with Not_found -> None with
-    | Some pb -> 
-      let s = Zproj (pb.proj_npars, pb.proj_arg, p) in
-	Some (c, s)
-    | None -> None)
-  (* else None *)
+  let pb = lookup_projection p (infos_env infos) in
+  let s = Zproj (pb.proj_npars, pb.proj_arg, p) in
+    (c, s)
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
@@ -297,35 +293,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 		| None -> raise NotConvertible) in
             eqappr univ cv_pb infos app1 app2)
 	  
-    | (FProj (p1,c1), FProj (p2, c2)) ->
-      (* Projections: prefer unfolding to first-order unification,
-	 which will happen naturally if the terms c1, c2 are not in constructor
-	 form *)
-      (match unfold_projection infos p1 c1 with
-      | Some (def1,s1) -> 
-	eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2
-      | None ->
-	match unfold_projection infos p2 c2 with
-	| Some (def2,s2) ->
-	  eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
-	| None -> 
-          if Names.eq_con_chk p1 p2 && compare_stack_shape v1 v2 then
-	    let () = ccnv univ CONV infos el1 el2 c1 c2 in
-	      convert_stacks univ infos lft1 lft2 v1 v2
-	  else (* Two projections in WHNF: unfold *)
-	    raise NotConvertible)
-
-    | (FProj (p1,c1), t2) ->
-      (match unfold_projection infos p1 c1 with
-      | Some (def1,s1) ->
-         eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2
-      | None -> raise NotConvertible)
-      
+    | (FProj (p1,c1), _) ->
+      let (def1, s1) = unfold_projection infos p1 c1 in
+        eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2
+	  
     | (_, FProj (p2,c2)) ->
-      (match unfold_projection infos p2 c2 with
-      | Some (def2,s2) -> 
-         eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
-      | None -> raise NotConvertible)
+      let (def2, s2) = unfold_projection infos p2 c2 in
+        eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
 
     (* other constructors *)
     | (FLambda _, FLambda _) ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e9f84391b6..0257259340 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -989,10 +989,9 @@ let local_whd_state_gen flags sigma =
       | _ -> s)
 
     | Proj (p,c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) ->
-      (match (lookup_constant p (Global.env ())).Declarations.const_proj with
-      | None -> assert false
-      | Some pb -> whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
-        :: stack))
+      (let pb = lookup_projection p (Global.env ()) in
+	 whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
+           :: stack))
 
     | Case (ci,p,d,lf) ->
       whrec (d, Stack.Case (ci,p,lf,Cst_stack.empty) :: stack)