1 files changed, 75 insertions, 177 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ba0502ca45..418ea271cd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -121,10 +121,10 @@ module ReductionBehaviour = struct
     let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
 
   let discharge = function
-    | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
+    | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) ->
       let b =
-        if Lib.is_in_section (ConstRef c) then
-          let vars, _, _ = Lib.section_segment_of_constant c in
+        if Lib.is_in_section gr then
+          let vars = Lib.variable_section_segment_of_reference gr in
           let extra = List.length vars in
           let nargs' =
              if b.b_nargs = max_int then max_int
@@ -284,8 +284,6 @@ sig
   | Proj of int * int * projection * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
-  | Shift of int
-  | Update of 'a
   and 'a t = 'a member list
 
   exception IncompatibleFold2
@@ -296,12 +294,12 @@ sig
   val append_app : 'a array -> 'a t -> 'a t
   val decomp : 'a t -> ('a * 'a t) option
   val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
-  val equal : ('a * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool)
-    -> 'a t -> 'a t -> (int * int) option
+  val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool)
+    -> 'a t -> 'a t -> bool
   val compare_shape : 'a t -> 'a t -> bool
   val map : ('a -> 'a) -> 'a t -> 'a t
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
-    constr t -> constr t -> 'a * int * int
+    constr t -> constr t -> 'a
   val append_app_list : 'a list -> 'a t -> 'a t
   val strip_app : 'a t -> 'a t * 'a t
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
@@ -343,8 +341,6 @@ struct
   | Proj of int * int * projection * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
-  | Shift of int
-  | Update of 'a
   and 'a t = 'a member list
 
   let rec pr_member pr_c member =
@@ -367,8 +363,6 @@ struct
       ++ pr_comma () ++
 	prlist_with_sep pr_semicolon int remains ++
 	pr_comma () ++ pr pr_c params ++ str ")"
-    | Shift i -> str "ZShift(" ++ int i ++ str ")"
-    | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")"
   and pr pr_c l =
     let open Pp in
     prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l
@@ -403,54 +397,42 @@ struct
     else (l.(j), sk)
 
   let equal f f_fix sk1 sk2 =
-    let equal_cst_member x lft1 y lft2 =
+    let equal_cst_member x y =
       match x, y with
       | Cst_const (c1,u1), Cst_const (c2, u2) ->
-	Constant.equal c1 c2 && Univ.Instance.equal u1 u2
+        Constant.equal c1 c2 && Univ.Instance.equal u1 u2
       | Cst_proj p1, Cst_proj p2 ->
-	Constant.equal (Projection.constant p1) (Projection.constant p2)
+        Constant.equal (Projection.constant p1) (Projection.constant p2)
       | _, _ -> false
     in
-    let rec equal_rec sk1 lft1 sk2 lft2  =
+    let rec equal_rec sk1 sk2 =
       match sk1,sk2 with
-      | [],[] -> Some (lft1,lft2)
-      | (Update _ :: _, _ | _, Update _ :: _) -> assert false
-      | Shift k :: s1, _ -> equal_rec  s1  (lft1+k)  sk2 lft2
-      | _, Shift k :: s2 -> equal_rec sk1 lft1 s2 (lft2+k)
+      | [],[] -> true
       | App a1 :: s1, App a2 :: s2 ->
-	let t1,s1' = decomp_node_last a1 s1 in
-	let t2,s2' = decomp_node_last a2 s2 in
-	if f (t1,lft1) (t2,lft2) then equal_rec s1' lft1 s2' lft2 else None
+        let t1,s1' = decomp_node_last a1 s1 in
+        let t2,s2' = decomp_node_last a2 s2 in
+        (f t1 t2) && (equal_rec s1' s2')
       | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 ->
-	if f (t1,lft1) (t2,lft2) && CArray.equal (fun x y -> f (x,lft1) (y,lft2)) a1 a2
-	then equal_rec s1 lft1 s2 lft2
-	else None
+        f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
       | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) ->
-	if Int.equal n1 n2 && Int.equal m1 m2
-	  && Constant.equal (Projection.constant p) (Projection.constant p2)
-	then equal_rec s1 lft1 s2 lft2
-	else None
+         Int.equal n1 n2 && Int.equal m1 m2
+           && Constant.equal (Projection.constant p) (Projection.constant p2)
+           && equal_rec s1 s2
       | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
-	if f_fix (f1,lft1) (f2,lft2) then
-	  match equal_rec (List.rev s1) lft1 (List.rev s2) lft2 with
-	  | None -> None
-	  | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2'
-	else None
+        f_fix f1 f2
+          && equal_rec (List.rev s1) (List.rev s2)
+          && equal_rec s1' s2'
       | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' ->
-	if equal_cst_member c1 lft1 c2 lft2 then
-	  match equal_rec (List.rev params1) lft1 (List.rev params2) lft2 with
-	  | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2'
-	  | None -> None
-	else None
-      | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> None
-    in equal_rec (List.rev sk1) 0 (List.rev sk2) 0
+        equal_cst_member c1 c2
+          && equal_rec (List.rev params1) (List.rev params2)
+          && equal_rec s1' s2'
+      | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> false
+    in equal_rec (List.rev sk1) (List.rev sk2)
 
   let compare_shape stk1 stk2 =
     let rec compare_rec bal stk1 stk2 =
       match (stk1,stk2) with
 	([],[]) -> Int.equal bal 0
-      | ((Update _|Shift _)::s1, _) -> compare_rec bal s1 stk2
-      | (_, (Update _|Shift _)::s2) -> compare_rec bal stk1 s2
       | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2
       | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2
       | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
@@ -466,40 +448,29 @@ struct
 
   exception IncompatibleFold2
   let fold2 f o sk1 sk2 =
-    let rec aux o lft1 sk1 lft2 sk2 =
-      let fold_array =
-	Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y))
-      in
+    let rec aux o sk1 sk2 =
       match sk1,sk2 with
-      | [], [] -> o,lft1,lft2
-      | Shift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2
-      | _, Shift n :: q2 -> aux o lft1 sk1 (lft2+n) q2
+      | [], [] -> o
       | App n1 :: q1, App n2 :: q2 ->
-	 let t1,l1 = decomp_node_last n1 q1 in
-	 let t2,l2 = decomp_node_last n2 q2 in
-	 aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
-	     lft1 l1 lft2 l2
+        let t1,l1 = decomp_node_last n1 q1 in
+        let t2,l2 = decomp_node_last n2 q2 in
+        aux (f o t1 t2) l1 l2
       | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 ->
-	aux (fold_array
-	       (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
-	       a1 a2) lft1 q1 lft2 q2
+        aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2
       | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 ->
-	aux o lft1 q1 lft2 q2
+        aux o q1 q2
       | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 ->
-	let (o',lft1',lft2') = aux (fold_array (fold_array o b1 b2) a1 a2)
-	  lft1 (List.rev s1) lft2 (List.rev s2) in
-	aux o' lft1' q1 lft2' q2
+        let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in
+        aux o' q1 q2
       | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 ->
-	let (o',lft1',lft2') =
-	  aux o lft1 (List.rev params1) lft2 (List.rev params2)
-	in aux o' lft1' q1 lft2' q2
-      | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
-	raise IncompatibleFold2
-    in aux o 0 (List.rev sk1) 0 (List.rev sk2)
+        let o' = aux o (List.rev params1) (List.rev params2) in
+        aux o' q1 q2
+      | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
+              raise IncompatibleFold2
+    in aux o (List.rev sk1) (List.rev sk2)
 
   let rec map f x = List.map (function
-			       | Update _ -> assert false
-			       | (Proj (_,_,_,_) | Shift _) as e -> e
+                               | (Proj (_,_,_,_)) as e -> e
 			       | App (i,a,j) ->
 				  let le = j - i + 1 in
 				  App (0,Array.map f (Array.sub a i le), le-1)
@@ -516,18 +487,15 @@ struct
 
   let rec args_size = function
     | App (i,_,j)::s -> j + 1 - i + args_size s
-    | Shift(_)::s -> args_size s
-    | Update(_)::s -> args_size s
     | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0
 
   let strip_app s =
     let rec aux out = function
-      | ( App _ | Shift _ as e) :: s -> aux (e :: out) s
+      | ( App _ as e) :: s -> aux (e :: out) s
       | s -> List.rev out,s
     in aux [] s
   let strip_n_app n s =
     let rec aux n out = function
-      | Shift k as e :: s -> aux n (e :: out) s
       | App (i,a,j) as e :: s ->
 	 let nb = j  - i + 1 in
 	 if n >= nb then
@@ -552,14 +520,12 @@ struct
   let list_of_app_stack s =
     let rec aux = function
       | App (i,a,j) :: s ->
-	 let (k,(args',s')) = aux s in
-	 let a' = Array.map (Vars.lift k) (Array.sub a i (j - i + 1)) in
-	 k,(Array.fold_right (fun x y -> x::y) a' args', s')
-      | Shift n :: s ->
-	 let (k,(args',s')) = aux s in (k+n,(args', s'))
-      | s -> (0,([],s)) in
-    let (lft,(out,s')) = aux s in
-    let init = match s' with [] when Int.equal lft 0 -> true | _ -> false in
+        let (args',s') = aux s in
+        let a' = Array.sub a i (j - i + 1) in
+        (Array.fold_right (fun x y -> x::y) a' args', s')
+      | s -> ([],s) in
+    let (out,s') = aux s in
+    let init = match s' with [] -> true | _ -> false in
     Option.init init out
 
   let assign s p c =
@@ -568,20 +534,18 @@ struct
     | None -> assert false
 
   let tail n0 s0 =
-    let rec aux lft n s =
-      let out s = if Int.equal lft 0 then s else Shift lft :: s in
-      if Int.equal n 0 then out s else
+    let rec aux n s =
+      if Int.equal n 0 then s else
 	match s with
       | App (i,a,j) :: s ->
 	 let nb = j  - i + 1 in
 	 if n >= nb then
-	   aux lft (n - nb) s
+           aux (n - nb) s
 	 else
 	   let p = i+n in
 	   if j >= p then App(p,a,j)::s else s
-	| Shift k :: s' -> aux (lft+k) n s'
 	| _ -> raise (Invalid_argument "Reductionops.Stack.tail")
-    in aux 0 n0 s0
+    in aux n0 s0
 
   let nth s p =
     match strip_n_app p s with
@@ -627,11 +591,9 @@ struct
     zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
   | f, (Cst (cst,_,_,params,_)::s) ->
     zip (constr_of_cst_member cst (params @ (append_app [|f|] s)))
-  | f, (Shift n::s) -> zip (lift n f, s)
   | f, (Proj (n,m,p,cst_l)::s) when refold ->
     zip (best_state sigma (mkProj (p,f),s) cst_l)
   | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s)
-  | _, (Update _::_) -> assert false
   in
   zip s
 
@@ -868,11 +830,9 @@ let _ = Goptions.declare_bool_option {
 }
 
 let equal_stacks sigma (x, l) (y, l') =
-  let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in
-  let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in
-    match Stack.equal f_equal eq_fix l l' with
-    | None -> false
-    | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) 
+  let f_equal x y = eq_constr sigma x y in
+  let eq_fix a b = f_equal (mkFix a) (mkFix b) in
+  Stack.equal f_equal eq_fix l l' && f_equal x y
 
 let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let open Context.Named.Declaration in
@@ -1074,7 +1034,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 		(arg,
 		 Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''')
 	  end
-	|_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false
+        |_, (Stack.App _)::_ -> assert false
 	|_, _ -> fold ()
       else fold ()
 
@@ -1155,7 +1115,7 @@ let local_whd_state_gen flags sigma =
 	|args, (Stack.Fix (f,s',cst)::s'') when use_fix ->
 	  let x' = Stack.zip sigma (x,args) in
 	  whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s''))
-	|_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false
+        |_, (Stack.App _|Stack.Cst _)::_ -> assert false
 	|_, _ -> s
       else s
 
@@ -1281,9 +1241,9 @@ let clos_whd_flags flgs env sigma t =
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
 
-let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
-let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ())
-let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ())
+let nf_beta = clos_norm_flags CClosure.beta
+let nf_betaiota = clos_norm_flags CClosure.betaiota
+let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta
 let nf_all env sigma =
   clos_norm_flags CClosure.all env sigma
 
@@ -1292,11 +1252,11 @@ let nf_all env sigma =
 (*                         Conversion                               *)
 (********************************************************************)
 (*
-let fkey = Profile.declare_profile "fhnf";;
-let fhnf info v = Profile.profile2 fkey fhnf info v;;
+let fkey = CProfile.declare_profile "fhnf";;
+let fhnf info v = CProfile.profile2 fkey fhnf info v;;
 
-let fakey = Profile.declare_profile "fhnf_apply";;
-let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
+let fakey = CProfile.declare_profile "fhnf_apply";;
+let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;;
 *)
 
 let is_transparent e k =
@@ -1306,7 +1266,7 @@ let is_transparent e k =
 
 (* Conversion utility functions *)
 
-type conversion_test = constraints -> constraints
+type conversion_test = Constraint.t -> Constraint.t
 
 let pb_is_equal pb = pb == Reduction.CONV
 
@@ -1364,79 +1324,17 @@ let sigma_compare_instances ~flex i0 i1 sigma =
      | Univ.UniverseInconsistency _ ->
 	raise Reduction.NotConvertible
 
-let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
-  let len_instance =
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind)
-  in
-  let ind_sbctx =  Univ.ACumulativityInfo.subtyp_context uinfind  in
-  if not ((len_instance = Univ.Instance.length u) &&
-          (len_instance = Univ.Instance.length u')) then
-     anomaly (Pp.str "Invalid inductive subtyping encountered!")
-  else
-    let comp_cst =
-      let comp_subst = (Univ.Instance.append u u') in
-      Univ.AUContext.instantiate comp_subst ind_sbctx
-    in
-    let comp_cst =
-      match cv_pb with
-        Reduction.CONV -> 
-        let comp_subst = (Univ.Instance.append u' u) in
-        let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in
-        Univ.Constraint.union comp_cst comp_cst'
-      | Reduction.CUMUL -> comp_cst
-    in
-    try Evd.add_constraints sigma comp_cst
-    with Evd.UniversesDiffer
-       | Univ.UniverseInconsistency _ ->
-      raise Reduction.NotConvertible
-
-let sigma_conv_inductives
-    cv_pb (mind, ind) u1 sv1 u2 sv2 sigma =
-  try sigma_compare_instances ~flex:false u1 u2 sigma with
-    Reduction.NotConvertible ->
-    match mind.Declarations.mind_universes with
-    | Declarations.Monomorphic_ind _ ->
-      raise Reduction.NotConvertible
-    | Declarations.Polymorphic_ind _ ->
-      raise Reduction.NotConvertible
-    | Declarations.Cumulative_ind cumi ->
-      let num_param_arity =
-        mind.Declarations.mind_nparams + 
-        mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-      in
-      if not (num_param_arity = sv1 && num_param_arity = sv2) then
-        raise Reduction.NotConvertible
-      else
-        sigma_check_inductive_instances cv_pb cumi u1 u2 sigma 
-
-let sigma_conv_constructors
-    (mind, ind, cns) u1 sv1 u2 sv2 sigma =
-  try sigma_compare_instances ~flex:false u1 u2 sigma with
-    Reduction.NotConvertible ->
-    match mind.Declarations.mind_universes with
-    | Declarations.Monomorphic_ind _ ->
-      raise Reduction.NotConvertible
-    | Declarations.Polymorphic_ind _ ->
-      raise Reduction.NotConvertible
-    | Declarations.Cumulative_ind cumi ->
-      let num_cnstr_args =
-        let nparamsctxt =
-          mind.Declarations.mind_nparams + 
-          mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-        in
-        nparamsctxt + 
-        mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
-      in
-      if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
-        raise Reduction.NotConvertible
-      else
-        sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma
+let sigma_check_inductive_instances csts sigma =
+  try Evd.add_constraints sigma csts
+  with Evd.UniversesDiffer
+     | Univ.UniverseInconsistency _ ->
+    raise Reduction.NotConvertible
 
 let sigma_univ_state = 
-  { Reduction.compare = sigma_compare_sorts;
-    Reduction.compare_instances = sigma_compare_instances;
-    Reduction.conv_inductives = sigma_conv_inductives;
-    Reduction.conv_constructors = sigma_conv_constructors}
+  let open Reduction in
+  { compare_sorts = sigma_compare_sorts;
+    compare_instances = sigma_compare_instances;
+    compare_cumul_instances = sigma_check_inductive_instances; }
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
@@ -1685,7 +1583,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 	if isConstruct sigma t_o then
 	  whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
 	else s,csts'
-      |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts'
+      |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts'
   in whrec csts s
 
 let find_conclusion env sigma =