List.fold_left (aux ctx) (i::acc) l)
| t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t
in
- HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
+ HExtlib.list_uniq (List.sort Stdlib.compare (aux context [] term))
;;
module NCicHash =
apply_subst subst () (NCicSubstitution.lift status n t)) l))))
| t -> NCicUtils.map status (fun _ () -> ()) () (apply_subst subst) t
in
- (if fix_projections then fire_projection_redex status () else fun x -> x)
- (clean_or_fix_dependent_abstrations status context (apply_subst subst () t))
+ let t = apply_subst subst () t in
+ let t = clean_or_fix_dependent_abstrations status context t in
+ if fix_projections then
+ fire_projection_redex status () t
+ else
+ t
;;
let apply_subst_context status ~fix_projections subst context =
;;
let set_kind newkind attrs =
- newkind :: List.filter (fun x -> not (is_kind x)) attrs
+ (newkind :> NCic.meta_attr) :: List.filter (fun x -> not (is_kind x)) attrs
;;
let max_kind k1 k2 =
module OT =
struct
type t = int * NCic.conjecture
- let compare (i,_) (j,_) = Pervasives.compare i j
+ let compare (i,_) (j,_) = Stdlib.compare i j
end
module MS = HTopoSort.Make(OT)