diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 244b8e60b..6fde86837 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -83,7 +83,7 @@ let declare_reduction_effect funkey f = (** A function to set the value of the print function *) let set_reduction_effect x funkey = - let termkey = Universes.constr_of_global x in + let termkey = UnivGen.constr_of_global x in Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey)) @@ -104,7 +104,7 @@ module ReductionBehaviour = struct type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ] type req = | ReqLocal - | ReqGlobal of global_reference * (int list * int * flag list) + | ReqGlobal of GlobRef.t * (int list * int * flag list) let load _ (_,(_,(r, b))) = table := Refmap.add r b !table @@ -701,18 +701,18 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with let magicaly_constant_of_fixbody env sigma reference bd = function | Name.Anonymous -> bd | Name.Name id -> - let open Universes in + let open UnivProblem in try let (cst_mod,cst_sect,_) = Constant.repr3 reference in let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in - let (cst, u), ctx = fresh_constant_instance env cst in + let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in begin match csts with | Some csts -> - let subst = Constraints.fold (fun cst acc -> + let subst = Set.fold (fun cst acc -> let l, r = match cst with | ULub (u, v) | UWeak (u, v) -> u, v | UEq (u, v) | ULe (u, v) -> @@ -1404,7 +1404,7 @@ let plain_instance sigma s c = | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) | App (f,l) when isCast sigma f -> let (f,_,t) = destCast sigma f in - let l' = CArray.Fun1.smartmap irec n l in + let l' = Array.Fun1.Smart.map irec n l in (match EConstr.kind sigma f with | Meta p -> (* Don't flatten application nodes: this is used to extract a @@ -1413,7 +1413,7 @@ let plain_instance sigma s c = (try let g = Metamap.find p s in match EConstr.kind sigma g with | App _ -> - let l' = CArray.Fun1.smartmap lift 1 l' in + let l' = Array.Fun1.Smart.map lift 1 l' in mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) |