Remove redundant env argument to Reduction.ccnv

The infos already contain the env. Note that it was only actually used
in the 2 lookup_mind lines.

1 files changed, 46 insertions, 46 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2bf9f43a5..6dd364789 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -309,11 +309,11 @@ let unfold_projection infos p c =
   else None
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
-let rec ccnv env cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
-  eqappr env cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
+  eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
 
 (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
-and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
+and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   Control.check_for_interrupt ();
   (* First head reduce both terms *)
   let whd = whd_stack (infos_with_reds infos betaiotazeta) in
@@ -338,13 +338,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	       sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if Int.equal n m
-	       then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+               then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
                else raise NotConvertible
 	   | _ -> raise NotConvertible)
     | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
         if Evar.equal ev1 ev2 then
-          let cuniv = convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv in
-          convert_vect env l2r infos el1 el2
+          let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
+          convert_vect l2r infos el1 el2
             (Array.map (mk_clos env1) args1)
             (Array.map (mk_clos env2) args2) cuniv
         else raise NotConvertible
@@ -352,14 +352,14 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     (* 2 index known to be bound to no constant *)
     | (FRel n, FRel m) ->
         if Int.equal (reloc_rel n el1) (reloc_rel m el2)
-        then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+        then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
     (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
       (try
 	 let cuniv = conv_table_key infos fl1 fl2 cuniv in
-	   convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with NotConvertible | Univ.UniverseInconsistency _ ->
            (* else the oracle tells which constant is to be expanded *)
 	 let oracle = CClosure.oracle_of_infos infos in
@@ -379,7 +379,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
                | Some def1 -> ((lft1, (def1, v1)), appr2)
 	       | None -> raise NotConvertible) 
 	 in
-           eqappr env cv_pb l2r infos app1 app2 cuniv)
+           eqappr cv_pb l2r infos app1 app2 cuniv)
 
     | (FProj (p1,c1), FProj (p2, c2)) ->
       (* Projections: prefer unfolding to first-order unification,
@@ -387,42 +387,42 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	 form *)
       (match unfold_projection infos p1 c1 with
       | Some (def1,s1) -> 
-	eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
+        eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
       | None ->
 	match unfold_projection infos p2 c2 with
 	| Some (def2,s2) ->
-	  eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
+          eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
 	| None -> 
           if Constant.equal (Projection.constant p1) (Projection.constant p2)
 	     && compare_stack_shape v1 v2 then
-	    let u1 = ccnv env CONV l2r infos el1 el2 c1 c2 cuniv in
-	      convert_stacks env l2r infos lft1 lft2 v1 v2 u1
+            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)
 
     | (FProj (p1,c1), t2) ->
       (match unfold_projection infos p1 c1 with
       | Some (def1,s1) ->
-         eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
+         eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
       | None -> 
 	 (match t2 with 
 	  | FFlex fl2 ->
 	     (match unfold_reference infos fl2 with
               | Some def2 ->
-		 eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
+                 eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
       
     | (t1, FProj (p2,c2)) ->
       (match unfold_projection infos p2 c2 with
       | Some (def2,s2) -> 
-         eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
+         eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
       | None -> 
 	 (match t1 with 
 	  | FFlex fl1 ->
 	     (match unfold_reference infos fl1 with
               | Some def1 ->
-		 eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
+                 eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
       
@@ -434,15 +434,15 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	  anomaly (Pp.str "conversion was given ill-typed terms (FLambda).");
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
-        let cuniv = ccnv env CONV l2r infos el1 el2 ty1 ty2 cuniv in
-        ccnv env CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
+        let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
+        ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
 
     | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
 	  anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
 	(* Luo's system *)
-        let cuniv = ccnv env CONV l2r infos el1 el2 c1 c'1 cuniv in
-        ccnv env cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
+        let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
+        ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
 
     (* Eta-expansion on the fly *)
     | (FLambda _, _) ->
@@ -452,7 +452,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           anomaly (Pp.str "conversion was given unreduced term (FLambda).")
         in
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
-	eqappr env CONV l2r infos
+        eqappr CONV l2r infos
 	  (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
     | (_, FLambda _) ->
         let () = match v2 with
@@ -461,34 +461,34 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	  anomaly (Pp.str "conversion was given unreduced term (FLambda).")
 	in
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
-	eqappr env CONV l2r infos
+        eqappr CONV l2r infos
 	  (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
 	
     (* only one constant, defined var or defined rel *)
     | (FFlex fl1, c2)      ->
        (match unfold_reference infos fl1 with
 	| Some def1 ->
-	   eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
+           eqappr cv_pb l2r infos (lft1, (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 env l2r infos lft1 lft2 v1 v2 cuniv
+              in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
 	      with Not_found -> raise NotConvertible)
 	   | _ -> raise NotConvertible)
        
     | (c1, FFlex fl2)      ->
        (match unfold_reference infos fl2 with
         | Some def2 ->
-	   eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
+           eqappr cv_pb l2r infos appr1 (lft2, (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 env l2r infos lft1 lft2 v1 v2 cuniv
+                   in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
 	       with Not_found -> raise NotConvertible)
 	   | _ -> raise NotConvertible)
        
@@ -497,9 +497,9 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       if eq_ind ind1 ind2 then
         if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
           let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
-          let mind = Environ.lookup_mind (fst ind1) env in
+          let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
           let cuniv =
             match mind.Declarations.mind_universes with
             | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
@@ -508,16 +508,16 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
               convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
                 u2 (CClosure.stack_args_size v2) cuniv
           in
-          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
       if Int.equal j1 j2 && eq_ind ind1 ind2 then
         if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
           let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
-          let mind = Environ.lookup_mind (fst ind1) env in
+          let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
           let cuniv =
             match mind.Declarations.mind_universes with
             | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
@@ -527,7 +527,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
                 (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
                 u2 (CClosure.stack_args_size v2) cuniv
           in
-          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 	  
     (* Eta expansion of records *)
@@ -535,14 +535,14 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       (try
     	 let v1, v2 =
     	   eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
-    	 in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+         in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (_, FConstruct ((ind2,j2),u2)) ->
       (try
     	 let v2, v1 =
     	   eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
-    	 in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+         in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
@@ -553,11 +553,11 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let fty2 = Array.map (mk_clos e2) tys2 in
           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-	  let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
+          let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
           let cuniv =
-            convert_vect env l2r infos
+            convert_vect l2r infos
 	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
-          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
     | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
@@ -568,11 +568,11 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let fty2 = Array.map (mk_clos e2) tys2 in
           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-          let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
+          let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
           let cuniv =
-	    convert_vect env l2r infos
+            convert_vect l2r infos
 	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
-          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
@@ -583,13 +583,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
      (* In all other cases, terms are not convertible *)
      | _ -> raise NotConvertible
 
-and convert_stacks env l2r infos lft1 lft2 stk1 stk2 cuniv =
+and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks
-    (fun (l1,t1) (l2,t2) cuniv -> ccnv env CONV l2r infos l1 l2 t1 t2 cuniv)
+    (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
     (eq_ind)
     lft1 stk1 lft2 stk2 cuniv
 
-and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv =
+and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
   let lv1 = Array.length v1 in
   let lv2 = Array.length v2 in
   if Int.equal lv1 lv2
@@ -597,7 +597,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv =
     let rec fold n cuniv =
       if n >= lv1 then cuniv
       else
-        let cuniv = ccnv env CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
+        let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
         fold (n+1) cuniv in
     fold 0 cuniv
   else raise NotConvertible
@@ -605,7 +605,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv =
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in
-  ccnv env cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
+  ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
 
 
 let check_eq univs u u' =