aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/assumptions.ml25
-rw-r--r--toplevel/class.ml2
-rw-r--r--toplevel/command.ml8
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/himsg.ml2
-rw-r--r--toplevel/indschemes.ml4
-rw-r--r--toplevel/obligations.ml6
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/search.ml4
-rw-r--r--toplevel/vernacentries.ml2
10 files changed, 39 insertions, 18 deletions
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 8865cd646..deb2ed3e0 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -144,6 +144,27 @@ let label_of = function
| ConstructRef ((kn,_),_) -> pi3 (repr_mind kn)
| VarRef id -> Label.of_id id
+let fold_constr_with_full_binders g f n acc c =
+ let open Context.Rel.Declaration in
+ match kind_of_term c with
+ | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc
+ | Cast (c,_, t) -> f n (f n acc c) t
+ | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Proj (p,c) -> f n acc c
+ | Evar (_,l) -> Array.fold_left (f n) acc l
+ | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | CoFix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+
let rec traverse current ctx accu t = match kind_of_term t with
| Var id ->
let body () = id |> Global.lookup_named |> NamedDecl.get_value in
@@ -166,10 +187,10 @@ let rec traverse current ctx accu t = match kind_of_term t with
traverse_object
~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
| _ ->
- Termops.fold_constr_with_full_binders
+ fold_constr_with_full_binders
Context.Rel.add (traverse current) ctx accu t
end
-| _ -> Termops.fold_constr_with_full_binders
+| _ -> fold_constr_with_full_binders
Context.Rel.add (traverse current) ctx accu t
and traverse_object ?inhabits (curr, data, ax2ty) body obj =
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 0dc799014..46854e5c0 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -85,7 +85,7 @@ let uniform_cond nargs lt =
let rec aux = function
| (0,[]) -> true
| (n,t::l) ->
- let t = strip_outer_cast t in
+ let t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *) in
isRel t && Int.equal (destRel t) n && aux ((n-1),l)
| _ -> false
in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ef918ef8d..62bbd4b97 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -685,7 +685,7 @@ let is_recursive mie =
let rec is_recursive_constructor lift typ =
match Term.kind_of_term typ with
| Prod (_,arg,rest) ->
- Termops.dependent (mkRel lift) arg ||
+ not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) ||
is_recursive_constructor (lift+1) rest
| LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest
| _ -> false
@@ -813,11 +813,11 @@ let warn_non_full_mutual =
(fun (x,xge,y,yge,isfix,rest) ->
non_full_mutual_message x xge y yge isfix rest)
-let check_mutuality env isfix fixl =
+let check_mutuality env evd isfix fixl =
let names = List.map fst fixl in
let preorder =
List.map (fun (id,def) ->
- (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env id' def) names))
+ (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) names))
fixl in
let po = partial_order Id.equal preorder in
match List.filter (function (_,Inr _) -> true | _ -> false) po with
@@ -1144,7 +1144,7 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) =
check_evars_are_solved env evd (Evd.empty,evd);
if List.for_all Option.has_some fixdefs then begin
let fixdefs = List.map Option.get fixdefs in
- check_mutuality env isfix (List.combine fixnames fixdefs)
+ check_mutuality env evd isfix (List.combine fixnames fixdefs)
end
let interp_fixpoint l ntns =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 616afb91f..fae783ef0 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -170,7 +170,7 @@ val do_cofixpoint :
(** Utils *)
-val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
+val check_mutuality : Environ.env -> Evd.evar_map -> bool -> (Id.t * types) list -> unit
val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 891662b93..bfe86053e 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1090,7 +1090,7 @@ let error_ill_formed_inductive env c v =
let error_ill_formed_constructor env id c v nparams nargs =
let pv = pr_lconstr_env env Evd.empty v in
- let atomic = Int.equal (nb_prod c) 0 in
+ let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in
str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++
str "is not valid;" ++ brk(1,1) ++
strbrk (if atomic then "it must be " else "its conclusion must be ") ++
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 48521a8e5..3f818f960 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -313,7 +313,7 @@ let warn_cannot_build_congruence =
strbrk "Cannot build congruence scheme because eq is not found")
let declare_congr_scheme ind =
- if Hipattern.is_equality_type (mkInd ind) then begin
+ if Hipattern.is_equality_type Evd.empty (mkInd ind) (** FIXME *) then begin
if
try Coqlib.check_required_library Coqlib.logic_module_name; true
with e when CErrors.noncritical e -> false
@@ -472,7 +472,7 @@ let build_combined_scheme env schemes =
let (c, t) = List.hd defs in
let ctx, ind, nargs = find_inductive t in
(* Number of clauses, including the predicates quantification *)
- let prods = nb_prod t - (nargs + 1) in
+ let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in
let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
let relargs = rel_vect 0 prods in
let concls = List.rev_map
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 9ada04317..1d5e4a2fa 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -145,7 +145,7 @@ let rec chop_product n t =
if Int.equal n 0 then Some t
else
match kind_of_term t with
- | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
+ | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop (EConstr.of_constr b)) else None
| _ -> None
let evar_dependencies evm oev =
@@ -396,7 +396,7 @@ let subst_deps expand obls deps t =
(Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
let rec prod_app t n =
- match kind_of_term (Termops.strip_outer_cast t) with
+ match kind_of_term (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *) with
| Prod (_,_,b) -> subst1 n b
| LetIn (_, b, t, b') -> prod_app (subst1 b b') n
| _ ->
@@ -521,7 +521,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
but doing it properly involves delta-reduction, and it finally
doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
- let m = Termops.nb_prod fixtype in
+ let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (** FIXME *) in
let ctx = fst (decompose_prod_n_assum m fixtype) in
List.map_i (fun i _ -> i) 0 ctx
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c43b32762..7dee4aae0 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -374,7 +374,7 @@ let structure_signature ctx =
let evm = Sigma.to_evar_map evm in
let new_tl = Util.List.map_i
(fun pos decl ->
- RelDecl.map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in
+ RelDecl.map_type (fun t -> Termops.replace_term evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t)) decl) 1 tl in
deps_to_evar evm new_tl in
deps_to_evar Evd.empty (List.rev ctx)
diff --git a/toplevel/search.ml b/toplevel/search.ml
index d319b2419..c0bcc403c 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -112,7 +112,7 @@ let generic_search glnumopt fn =
(** This function tries to see whether the conclusion matches a pattern. *)
(** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
let rec pattern_filter pat ref env typ =
- let typ = Termops.strip_outer_cast typ in
+ let typ = Termops.strip_outer_cast Evd.empty (EConstr.of_constr typ) (** FIXME *) in
if Constr_matching.is_matching env Evd.empty pat typ then true
else match kind_of_term typ with
| Prod (_, _, typ)
@@ -120,7 +120,7 @@ let rec pattern_filter pat ref env typ =
| _ -> false
let rec head_filter pat ref env typ =
- let typ = Termops.strip_outer_cast typ in
+ let typ = Termops.strip_outer_cast Evd.empty (EConstr.of_constr typ) (** FIXME *) in
if Constr_matching.is_matching_head env Evd.empty pat typ then true
else match kind_of_term typ with
| Prod (_, _, typ)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ede88399e..bbbdbdb67 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -107,7 +107,7 @@ let show_intro all =
let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
if not (List.is_empty gls) then begin
let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
- let l,_= decompose_prod_assum (Termops.strip_outer_cast (pf_concl gl)) in
+ let l,_= decompose_prod_assum (Termops.strip_outer_cast (project gl) (EConstr.of_constr (pf_concl gl))) in
if all then
let lid = Tactics.find_intro_names l gl in
Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 23:44:49 +0000