Remove an ununsed pattern and commented code in the kernel.

Reestablish completeness in conversion when Opaque primitive
projections are used.

3 files changed, 50 insertions, 45 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 6b5a6cdb9..e43e08865 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -80,7 +80,7 @@ let rel_context_tags ctx =
   let rec aux l = function
   | [] -> l
   | (_,Some _,_)::ctx -> aux (true::l) ctx
-  | (_,None _,_)::ctx -> aux (false::l) ctx
+  | (_,None,_)::ctx -> aux (false::l) ctx
   in aux [] ctx
 
 (*s Signatures of named hypotheses. Used for section variables and
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 9a7146890..64964f85e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -370,24 +370,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	| Some (def2,s2) ->
 	  eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
 	| None -> 
-          if Projection.equal p1 p2 && compare_stack_shape v1 v2 then
+          if Constant.equal (Projection.constant p1) (Projection.constant p2) 
+	    && compare_stack_shape v1 v2 then
 	    let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
 	      convert_stacks l2r infos lft1 lft2 v1 v2 u1
-	  else (* Two projections in WHNF: unfold *)
-	    raise NotConvertible)
+	  else raise NotConvertible)
 
-    | (FProj (p1,c1), t2) ->
-      (match unfold_projection infos p1 c1 with
-      | Some (def1,s1) ->
-         eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv
-      | None -> raise NotConvertible)
-      
-    | (_, FProj (p2,c2)) ->
-      (match unfold_projection infos p2 c2 with
-      | Some (def2,s2) -> 
-         eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
-      | None -> raise NotConvertible)
-      
     (* other constructors *)
     | (FLambda _, FLambda _) ->
         (* Inconsistency: we tolerate that v1, v2 contain shift and update but
@@ -428,31 +416,53 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     (* only one constant, defined var or defined rel *)
     | (FFlex fl1, c2)      ->
-        (match unfold_reference infos fl1 with
-           | Some def1 ->
-	       eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
-           | None -> 
-	     match c2 with
-	     | FConstruct ((ind2,j2),u2) ->
-	       (try
- 	     	  let v2, v1 =
- 	     	    eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
- 	     	  in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
- 	     	with Not_found -> raise NotConvertible)
-	     | _ -> raise NotConvertible)
-
+      (match unfold_reference infos fl1 with
+      | Some def1 ->
+	eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
+      | None -> 
+	match c2 with
+	| FConstruct ((ind2,j2),u2) ->
+	  (try
+ 	     let v2, v1 =
+ 	       eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
+ 	     in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ 	   with Not_found -> raise NotConvertible)
+	| FProj (p2,c2) ->
+	  (match unfold_projection infos p2 c2 with
+	  | Some (def2,s2) -> 
+	    eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
+	  | None -> raise NotConvertible)
+	| _ -> raise NotConvertible)
+	
     | (c1, FFlex fl2)      ->
-        (match unfold_reference infos fl2 with
-           | Some def2 ->
-	       eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
-           | None -> 
-	     match c1 with
-	     | FConstruct ((ind1,j1),u1) ->
- 	       (try let v1, v2 =
-	     	      eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
-	     	    in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-	     	with Not_found -> raise NotConvertible)
-	     | _ -> raise NotConvertible)
+      (match unfold_reference infos fl2 with
+      | Some def2 ->
+	eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
+      | None -> 
+	match c1 with
+	| FConstruct ((ind1,j1),u1) ->
+ 	  (try let v1, v2 =
+	     	 eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
+	       in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+	   with Not_found -> raise NotConvertible)
+	| FProj (p1,c1) ->
+	  (match unfold_projection infos p1 c1 with
+	  | Some (def1,s1) ->
+	    eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv
+	  | None -> raise NotConvertible)
+	| _ -> raise NotConvertible)
+	
+    | (FProj (p1,c1), t2) ->
+      (match unfold_projection infos p1 c1 with
+      | Some (def1,s1) ->
+         eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv
+      | None -> raise NotConvertible)
+	
+    | (t1, FProj (p2,c2)) ->
+      (match unfold_projection infos p2 c2 with
+      | Some (def2,s2) -> 
+	eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
+      | None -> raise NotConvertible)
 	  
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8f41f356d..79b3d518a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -65,11 +65,6 @@ let handle_side_effects env body side_eff =
       | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in
     let rec sub_body c u b i x = match kind_of_term x with
       | Const (c',u') when eq_constant c c' -> 
-	(* let subst =  *)
-	(*   Array.fold_left2 (fun subst l l' -> Univ.LMap.add l l' subst) *)
-	(*     Univ.LMap.empty (Instance.to_array u) (Instance.to_array u') *)
-	(* in  *)
-	(*   Vars.subst_univs_level_constr subst b *)
 	Vars.subst_instance_constr u' b
       | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
     let fix_body (c,cb,b) t =