diff options
34 files changed, 223 insertions, 220 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 73286f2c4..8940be09d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -47,10 +47,11 @@ let evd_comb2 f evdref x y = z let e_new_global evdref x = - evd_comb1 (Evd.fresh_global (Global.env())) evdref x + EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x) let new_global evd x = - Sigma.fresh_global (Global.env()) evd x + let Sigma (c, sigma, p) = Sigma.fresh_global (Global.env()) evd x in + Sigma (EConstr.of_constr c, sigma, p) (****************************************************) (* Expanding/testing/exposing existential variables *) @@ -230,7 +231,7 @@ let new_meta = let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in fun () -> incr meta_ctr; !meta_ctr -let mk_new_meta () = mkMeta(new_meta()) +let mk_new_meta () = EConstr.mkMeta(new_meta()) (* The list of non-instantiated existential declarations (order is important) *) @@ -396,6 +397,7 @@ let default_source = (Loc.ghost,Evar_kinds.InternalHole) let restrict_evar evd evk filter candidates = let evd = Sigma.to_evar_map evd in + let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let evd, evk' = Evd.restrict evk filter ?candidates evd in Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) @@ -408,6 +410,7 @@ let new_pure_evar_full evd evi = let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = let typ = EConstr.Unsafe.to_constr typ in let evd = Sigma.to_evar_map evd in + let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let evi = { @@ -437,7 +440,7 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin (* Converting the env into the sign of the evar to define *) let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in - let map c = EConstr.Unsafe.to_constr (subst2 subst vsubst (EConstr.of_constr c)) in + let map c = subst2 subst vsubst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = match filter with diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 5882f02b9..ea9599c8b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -17,18 +17,18 @@ open Environ (** [new_meta] is a generator of unique meta variables *) val new_meta : unit -> metavariable -val mk_new_meta : unit -> constr +val mk_new_meta : unit -> EConstr.constr (** {6 Creating a fresh evar given their type and context} *) val new_evar : env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:EConstr.constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.types -> (EConstr.constr, 'r) Sigma.sigma val new_pure_evar : named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:EConstr.constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.types -> (evar, 'r) Sigma.sigma @@ -37,7 +37,7 @@ val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma (** the same with side-effects *) val e_new_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:EConstr.constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.types -> EConstr.constr @@ -56,12 +56,12 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (EConstr.constr, 'r) Sigma.s val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> EConstr.constr val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> - constr list option -> (existential_key, 'r) Sigma.sigma + EConstr.constr list option -> (existential_key, 'r) Sigma.sigma (** Polymorphic constants *) -val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma -val e_new_global : evar_map ref -> Globnames.global_reference -> constr +val new_global : 'r Sigma.t -> Globnames.global_reference -> (EConstr.constr, 'r) Sigma.sigma +val e_new_global : evar_map ref -> Globnames.global_reference -> EConstr.constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -71,7 +71,7 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr as a telescope) is [sign] *) val new_evar_instance : named_context_val -> 'r Sigma.t -> EConstr.types -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> + ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:EConstr.constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.constr list -> (EConstr.constr, 'r) Sigma.sigma diff --git a/engine/termops.ml b/engine/termops.ml index 879d77de2..465832c10 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -210,12 +210,7 @@ let lookup_rel_id id sign = lookrec 1 sign (* Constructs either [forall x:t, c] or [let x:=b:t in c] *) -let mkProd_or_LetIn decl c = - let open RelDecl in - match decl with - | LocalAssum (na,t) -> mkProd (na, t, c) - | LocalDef (na,b,t) -> mkLetIn (na, b, t, c) - +let mkProd_or_LetIn = EConstr.mkProd_or_LetIn (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *) let mkProd_wo_LetIn decl c = let open EConstr in @@ -628,9 +623,10 @@ let vars_of_global_reference env gr = [m] is appropriately lifted through abstractions of [t] *) let dependent_main noevar univs sigma m t = + let open EConstr in let eqc x y = - if univs then not (Option.is_empty (EConstr.eq_constr_universes sigma x y)) - else EConstr.eq_constr_nounivs sigma x y + if univs then not (Option.is_empty (eq_constr_universes sigma x y)) + else eq_constr_nounivs sigma x y in let rec deprec m t = if eqc m t then @@ -638,13 +634,13 @@ let dependent_main noevar univs sigma m t = else match EConstr.kind sigma m, EConstr.kind sigma t with | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> - deprec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm))); + deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); CArray.Fun1.iter deprec m (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) - | _, Cast (c,_,_) when noevar && EConstr.isMeta sigma c -> () + | _, Cast (c,_,_) when noevar && isMeta sigma c -> () | _, Evar _ when noevar -> () - | _ -> EConstr.iter_with_binders sigma (fun c -> EConstr.Vars.lift 1 c) deprec m t + | _ -> EConstr.iter_with_binders sigma (fun c -> Vars.lift 1 c) deprec m t in try deprec m t; false with Occur -> true @@ -661,6 +657,7 @@ let dependent_in_decl sigma a decl = | LocalDef (_, body, t) -> dependent sigma a (EConstr.of_constr body) || dependent sigma a (EConstr.of_constr t) let count_occurrences sigma m t = + let open EConstr in let n = ref 0 in let rec countrec m t = if EConstr.eq_constr sigma m t then @@ -668,13 +665,13 @@ let count_occurrences sigma m t = else match EConstr.kind sigma m, EConstr.kind sigma t with | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> - countrec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm))); + countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); Array.iter (countrec m) (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) - | _, Cast (c,_,_) when EConstr.isMeta sigma c -> () + | _, Cast (c,_,_) when isMeta sigma c -> () | _, Evar _ -> () - | _ -> EConstr.iter_with_binders sigma (EConstr.Vars.lift 1) countrec m t + | _ -> EConstr.iter_with_binders sigma (Vars.lift 1) countrec m t in countrec m t; !n @@ -682,7 +679,7 @@ let count_occurrences sigma m t = (* Synonymous *) let occur_term = dependent -let pop t = EConstr.Unsafe.to_constr (EConstr.Vars.lift (-1) t) +let pop t = EConstr.Vars.lift (-1) t (***************************) (* bindings functions *) @@ -712,33 +709,35 @@ let collapse_appl sigma c = match EConstr.kind sigma c with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | _ -> EConstr.mkApp (f,cl2) in - EConstr.Unsafe.to_constr (collapse_rec f cl) - | _ -> EConstr.Unsafe.to_constr c + collapse_rec f cl + | _ -> c (* First utilities for avoiding telescope computation for subst_term *) let prefix_application sigma eq_fun (k,c) t = - let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in + let open EConstr in + let c' = collapse_appl sigma c and t' = collapse_appl sigma t in match EConstr.kind sigma c', EConstr.kind sigma t' with | App (f1,cl1), App (f2,cl2) -> let l1 = Array.length cl1 and l2 = Array.length cl2 in if l1 <= l2 - && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then - Some (EConstr.mkApp (EConstr.mkRel k, Array.sub cl2 l1 (l2 - l1))) + && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then + Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1))) else None | _ -> None let my_prefix_application sigma eq_fun (k,c) by_c t = - let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in + let open EConstr in + let c' = collapse_appl sigma c and t' = collapse_appl sigma t in match EConstr.kind sigma c', EConstr.kind sigma t' with | App (f1,cl1), App (f2,cl2) -> let l1 = Array.length cl1 and l2 = Array.length cl2 in if l1 <= l2 - && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then - Some (EConstr.mkApp ((EConstr.Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1))) + && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then + Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1))) else None | _ -> None @@ -754,7 +753,7 @@ let subst_term_gen sigma eq_fun c t = match prefix_application sigma eq_fun kc t with | Some x -> x | None -> - if eq_fun sigma c t then EConstr.mkRel k + if eq_fun sigma c t then mkRel k else EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t in @@ -775,7 +774,7 @@ let replace_term_gen sigma eq_fun c by_c in_t = EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c)) substrec kc t) in - EConstr.Unsafe.to_constr (substrec (0,c) in_t) + substrec (0,c) in_t let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t @@ -933,12 +932,11 @@ let filtering sigma env cv_pb c1 c2 = aux env cv_pb c1 c2; !evm let decompose_prod_letin sigma c = - let inj c = EConstr.Unsafe.to_constr c in let rec prodec_rec i l sigma c = match EConstr.kind sigma c with - | Prod (n,t,c) -> prodec_rec (succ i) (RelDecl.LocalAssum (n, inj t)::l) sigma c - | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n, inj d, inj t)::l) sigma c + | Prod (n,t,c) -> prodec_rec (succ i) (local_assum (n, t)::l) sigma c + | LetIn (n,d,t,c) -> prodec_rec (succ i) (local_def (n, d, t)::l) sigma c | Cast (c,_,_) -> prodec_rec i l sigma c - | _ -> i,l, inj c in + | _ -> i,l, c in prodec_rec 0 [] sigma c (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction @@ -969,7 +967,7 @@ let nb_prod_modulo_zeta sigma x = | _ -> n in count 0 x -let align_prod_letin sigma c a : Context.Rel.t * constr = +let align_prod_letin sigma c a = let (lc,_,_) = decompose_prod_letin sigma c in let (la,l,a) = decompose_prod_letin sigma a in if not (la >= lc) then invalid_arg "align_prod_letin"; @@ -980,21 +978,23 @@ let align_prod_letin sigma c a : Context.Rel.t * constr = (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *) (* Remplace 2 earlier buggish versions *) -let rec eta_reduce_head c = - match kind_of_term c with +let rec eta_reduce_head sigma c = + let open EConstr in + let open Vars in + match EConstr.kind sigma c with | Lambda (_,c1,c') -> - (match kind_of_term (eta_reduce_head c') with + (match EConstr.kind sigma (eta_reduce_head sigma c') with | App (f,cl) -> let lastn = (Array.length cl) - 1 in if lastn < 0 then anomaly (Pp.str "application without arguments") else - (match kind_of_term cl.(lastn) with + (match EConstr.kind sigma cl.(lastn) with | Rel 1 -> let c' = if Int.equal lastn 0 then f else mkApp (f, Array.sub cl 0 lastn) in - if noccurn 1 c' + if noccurn sigma 1 c' then lift (-1) c' else c | _ -> c) diff --git a/engine/termops.mli b/engine/termops.mli index 1699d600e..d7d9c743d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -12,6 +12,7 @@ open Pp open Names open Term +open EConstr open Environ (** printers *) @@ -20,59 +21,56 @@ val pr_sort_family : sorts_family -> std_ppcmds val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds (** debug printer: do not use to display terms to the casual user... *) -val set_print_constr : (env -> constr -> std_ppcmds) -> unit -val print_constr : constr -> std_ppcmds -val print_constr_env : env -> constr -> std_ppcmds +val set_print_constr : (env -> Constr.constr -> std_ppcmds) -> unit +val print_constr : Constr.constr -> std_ppcmds +val print_constr_env : env -> Constr.constr -> std_ppcmds val print_named_context : env -> std_ppcmds val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds (** about contexts *) -val push_rel_assum : Name.t * EConstr.types -> env -> env -val push_rels_assum : (Name.t * types) list -> env -> env -val push_named_rec_types : Name.t array * types array * 'a -> env -> env +val push_rel_assum : Name.t * types -> env -> env +val push_rels_assum : (Name.t * Constr.types) list -> env -> env +val push_named_rec_types : Name.t array * Constr.types array * 'a -> env -> env -val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types +val lookup_rel_id : Id.t -> Context.Rel.t -> int * Constr.constr option * Constr.types (** Associates the contents of an identifier in a [rel_context]. Raise [Not_found] if there is no such identifier. *) (** Functions that build argument lists matching a block of binders or a context. [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|] *) -val rel_vect : int -> int -> constr array -val rel_list : int -> int -> EConstr.constr list +val rel_vect : int -> int -> Constr.constr array +val rel_list : int -> int -> constr list (** iterators/destructors on terms *) val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types -val mkProd_wo_LetIn : Context.Rel.Declaration.t -> EConstr.types -> EConstr.types -val it_mkProd : EConstr.types -> (Name.t * EConstr.types) list -> EConstr.types -val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.constr +val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types +val it_mkProd : types -> (Name.t * types) list -> types +val it_mkLambda : constr -> (Name.t * types) list -> constr val it_mkProd_or_LetIn : types -> Context.Rel.t -> types -val it_mkProd_wo_LetIn : EConstr.types -> Context.Rel.t -> EConstr.types -val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr -val it_mkNamedProd_or_LetIn : EConstr.types -> Context.Named.t -> EConstr.types -val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types -val it_mkNamedLambda_or_LetIn : EConstr.constr -> Context.Named.t -> EConstr.constr +val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr +val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types +val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types +val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) -val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr +val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr (** {6 Generic iterators on constr} *) -val map_constr_with_named_binders : - (Name.t -> 'a -> 'a) -> - ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_binders_left_to_right : Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> EConstr.constr -> EConstr.constr) -> - 'a -> EConstr.constr -> EConstr.constr + ('a -> constr -> constr) -> + 'a -> constr -> constr val map_constr_with_full_binders : Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> EConstr.t -> EConstr.t) -> 'a -> EConstr.t -> EConstr.t + ('a -> constr -> constr) -> 'a -> constr -> constr (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to @@ -81,62 +79,61 @@ val map_constr_with_full_binders : index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *) -val fold_constr_with_binders : - Evd.evar_map -> ('a -> 'a) -> - ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b +val fold_constr_with_binders : Evd.evar_map -> + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -val fold_constr_with_full_binders : - Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b +val fold_constr_with_full_binders : Evd.evar_map -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b val iter_constr_with_full_binders : - (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> - constr -> unit + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> Constr.constr -> unit) -> 'a -> + Constr.constr -> unit (**********************************************************************) -val strip_head_cast : Evd.evar_map -> EConstr.t -> EConstr.t -val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> EConstr.constr +val strip_head_cast : Evd.evar_map -> constr -> constr +val drop_extra_implicit_args : Evd.evar_map -> constr -> constr (** occur checks *) exception Occur -val occur_meta : Evd.evar_map -> EConstr.t -> bool -val occur_existential : Evd.evar_map -> EConstr.t -> bool -val occur_meta_or_existential : Evd.evar_map -> EConstr.t -> bool -val occur_evar : Evd.evar_map -> existential_key -> EConstr.t -> bool -val occur_var : env -> Evd.evar_map -> Id.t -> EConstr.t -> bool +val occur_meta : Evd.evar_map -> constr -> bool +val occur_existential : Evd.evar_map -> constr -> bool +val occur_meta_or_existential : Evd.evar_map -> constr -> bool +val occur_evar : Evd.evar_map -> existential_key -> constr -> bool +val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> Context.Named.Declaration.t -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) -val local_occur_var : Evd.evar_map -> Id.t -> EConstr.t -> bool +val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool -val free_rels : Evd.evar_map -> EConstr.t -> Int.Set.t +val free_rels : Evd.evar_map -> constr -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) -val dependent : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_univs : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_univs_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_in_decl : Evd.evar_map -> EConstr.t -> Context.Named.Declaration.t -> bool -val count_occurrences : Evd.evar_map -> EConstr.t -> EConstr.t -> int -val collect_metas : Evd.evar_map -> EConstr.t -> int list -val collect_vars : Evd.evar_map -> EConstr.t -> Id.Set.t (** for visible vars only *) +val dependent : Evd.evar_map -> constr -> constr -> bool +val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool +val dependent_univs : Evd.evar_map -> constr -> constr -> bool +val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool +val dependent_in_decl : Evd.evar_map -> constr -> Context.Named.Declaration.t -> bool +val count_occurrences : Evd.evar_map -> constr -> constr -> int +val collect_metas : Evd.evar_map -> constr -> int list +val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t -val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous of dependent *) +val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *) (* Substitution of metavariables *) -type meta_value_map = (metavariable * constr) list -val subst_meta : meta_value_map -> constr -> constr -val isMetaOf : Evd.evar_map -> metavariable -> EConstr.constr -> bool +type meta_value_map = (metavariable * Constr.constr) list +val subst_meta : meta_value_map -> Constr.constr -> Constr.constr +val isMetaOf : Evd.evar_map -> metavariable -> constr -> bool (** Type assignment for metavariables *) -type meta_type_map = (metavariable * types) list +type meta_type_map = (metavariable * Constr.types) list (** [pop c] lifts by -1 the positive indexes in [c] *) -val pop : EConstr.t -> constr +val pop : constr -> constr (** {6 ... } *) (** Substitution of an arbitrary large term. Uses equality modulo @@ -145,37 +142,37 @@ val pop : EConstr.t -> constr (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq] as equality *) val subst_term_gen : Evd.evar_map -> - (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> EConstr.constr + (Evd.evar_map -> constr -> constr -> bool) -> constr -> constr -> constr (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] as equality *) val replace_term_gen : - Evd.evar_map -> (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> - EConstr.t -> EConstr.t -> EConstr.t -> constr + Evd.evar_map -> (Evd.evar_map -> constr -> constr -> bool) -> + constr -> constr -> constr -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) -val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.constr +val subst_term : Evd.evar_map -> constr -> constr -> constr (** [replace_term d e c] replaces [d] by [e] in [c] *) -val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr +val replace_term : Evd.evar_map -> constr -> constr -> constr -> constr (** Alternative term equalities *) val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool -val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool) -> - Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool -val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool -val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool (* FIXME rename: erases universes*) +val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> constr -> constr -> bool) -> + Reduction.conv_pb -> constr -> constr -> bool +val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> constr -> constr -> bool +val eq_constr : Evd.evar_map -> constr -> constr -> bool (* FIXME rename: erases universes*) -val eta_reduce_head : constr -> constr +val eta_reduce_head : Evd.evar_map -> constr -> constr (** Flattens application lists *) -val collapse_appl : Evd.evar_map -> EConstr.t -> constr +val collapse_appl : Evd.evar_map -> constr -> constr -val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t +val prod_applist : Evd.evar_map -> constr -> constr list -> constr (** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : Evd.evar_map -> EConstr.t -> EConstr.constr +val strip_outer_cast : Evd.evar_map -> constr -> constr exception CannotFilter @@ -185,32 +182,32 @@ exception CannotFilter (context,term), or raises [CannotFilter]. Warning: Outer-kernel sort subtyping are taken into account: c1 has to be smaller than c2 wrt. sorts. *) -type subst = (Context.Rel.t * constr) Evar.Map.t -val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst +type subst = (Context.Rel.t * Constr.constr) Evar.Map.t +val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> Constr.constr -> Constr.constr -> subst -val decompose_prod_letin : Evd.evar_map -> EConstr.t -> int * Context.Rel.t * constr -val align_prod_letin : Evd.evar_map -> EConstr.t -> EConstr.t -> Context.Rel.t * constr +val decompose_prod_letin : Evd.evar_map -> constr -> int * Context.Rel.t * constr +val align_prod_letin : Evd.evar_map -> constr -> constr -> Context.Rel.t * constr (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction gives {% $ %}n{% $ %} (casts are ignored) *) -val nb_lam : Evd.evar_map -> EConstr.t -> int +val nb_lam : Evd.evar_map -> constr -> int (** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : Evd.evar_map -> EConstr.t -> int +val nb_prod : Evd.evar_map -> constr -> int (** Similar to [nb_prod], but zeta-contracts let-in on the way *) -val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int +val nb_prod_modulo_zeta : Evd.evar_map -> constr -> int (** Get the last arg of a constr intended to be an application *) -val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr +val last_arg : Evd.evar_map -> constr -> constr (** Force the decomposition of a term as an applicative one *) -val decompose_app_vect : Evd.evar_map -> EConstr.t -> EConstr.constr * EConstr.constr array +val decompose_app_vect : Evd.evar_map -> constr -> constr * constr array -val adjust_app_list_size : EConstr.constr -> EConstr.constr list -> EConstr.constr -> EConstr.constr list -> - (EConstr.constr * EConstr.constr list * EConstr.constr * EConstr.constr list) -val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array -> - (EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array) +val adjust_app_list_size : constr -> constr list -> constr -> constr list -> + (constr * constr list * constr * constr list) +val adjust_app_array_size : constr -> constr array -> constr -> constr array -> + (constr * constr array * constr * constr array) (** name contexts *) type names_context = Name.t list @@ -239,15 +236,15 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env -val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list +val assums_of_rel_context : Context.Rel.t -> (Name.t * Constr.constr) list val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t -val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t +val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *) val map_rel_context_in_env : - (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t + (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t val map_rel_context_with_binders : - (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t + (int -> Constr.constr -> Constr.constr) -> Context.Rel.t -> Context.Rel.t val fold_named_context_both_sides : ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> Context.Named.t -> init:'a -> 'a @@ -256,10 +253,10 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t val clear_named_body : Id.t -> env -> env -val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list -val global_vars_set : env -> Evd.evar_map -> EConstr.t -> Id.Set.t +val global_vars : env -> Evd.evar_map -> constr -> Id.t list +val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t -val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option +val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) @@ -268,15 +265,15 @@ val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> I (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool -val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses +val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses -val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool +val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool -val isGlobalRef : Evd.evar_map -> EConstr.t -> bool +val isGlobalRef : Evd.evar_map -> constr -> bool -val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool +val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool -val is_Prop : Evd.evar_map -> EConstr.t -> bool +val is_Prop : Evd.evar_map -> constr -> bool (** Combinators on judgments *) @@ -285,5 +282,5 @@ val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) puns val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment (** {6 Functions to deal with impossible cases } *) -val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit +val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index c92ddf990..a7ff8e142 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -94,7 +94,6 @@ let find_global dir s = fun (evd,cstrs) -> let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in - let c = EConstr.of_constr c in let evd = Sigma.to_evar_map sigma in (evd, cstrs), c @@ -206,7 +205,6 @@ end) = struct fun (evd,cstrs) -> let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in - let c = EConstr.of_constr c in let evd = Sigma.to_evar_map sigma in (evd, cstrs), c @@ -215,7 +213,6 @@ end) = struct fun (evd,cstrs) -> let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in - let c = EConstr.of_constr c in let evd = Sigma.to_evar_map sigma in (evd, cstrs), c diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0d48b65d0..7a99c45a8 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -63,7 +63,6 @@ let rec decompose_term env sigma t= Array.fold_left (fun s t->Appli (s,t)) tf targs | Prod (_,a,_b) when noccurn sigma 1 _b -> let b = Termops.pop _b in - let b = EConstr.of_constr b in let sort_b = sf_of env sigma b in let sort_a = sf_of env sigma a in Appli(Appli(Product (sort_a,sort_b) , @@ -118,7 +117,6 @@ let rec pattern_of_constr env sigma c = List.fold_left Int.Set.union Int.Set.empty lrels | Prod (_,a,_b) when noccurn sigma 1 _b -> let b = Termops.pop _b in - let b = EConstr.of_constr b in let pa,sa = pattern_of_constr env sigma a in let pb,sb = pattern_of_constr env sigma b in let sort_b = sf_of env sigma b in diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index ddf013735..ae057b458 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -374,7 +374,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = match st'.st_it with Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} | This _ -> {st_it = This st.st_it;st_label=st.st_label} in - let thyps = fst (match_hyps blend nam2 (Termops.pop (EConstr.of_constr rest1)) hyps) in + let thyps = fst (match_hyps blend nam2 (Vars.lift (-1) rest1) hyps) in tparams,{pat_vars=tpatvars; pat_aliases=taliases; pat_constr=pat_pat; diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 96b991e1f..87bac2fe3 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -76,11 +76,13 @@ type kind_of_formula= | Forall of constr*constr | Atom of constr +let pop t = Vars.lift (-1) t + let kind_of_formula gl term = let normalize=special_nf gl in let cciterm=special_whd gl term in match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with - Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop b)) + Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop (EConstr.Unsafe.to_constr b))) |_-> match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b) diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 5520c7e35..7cbfb8e7d 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -24,6 +24,8 @@ exception UFAIL of constr*constr let strip_outer_cast t = EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *) +let pop t = Vars.lift (-1) t + let unif t1 t2= let evd = Evd.empty in (** FIXME *) let bige=Queue.create () @@ -62,7 +64,7 @@ let unif t1 t2= | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> - Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige + Queue.add (a,c) bige;Queue.add (pop b,pop d) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 188368082..cc29d68f5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -95,6 +95,7 @@ let list_chop ?(msg="") n l = with Failure (msg') -> failwith (msg ^ msg') +let pop t = Vars.lift (-1) t let make_refl_eq constructor type_of_t t = (* let refl_equal_term = Lazy.force refl_equal in *) @@ -289,7 +290,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = in let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in let sub = compute_substitution sub (fst t1) (fst t2) in - let end_of_type_with_pop = Termops.pop (EConstr.of_constr end_of_type) in (*the equation will be removed *) + let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) let new_end_of_type = (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 Can be safely replaced by the next comment for Ocaml >= 3.08.4 @@ -311,9 +312,9 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (Termops.pop (EConstr.of_constr end_of_type),ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) + (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) with Not_found -> - (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) + (Term.mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) 1 (new_end_of_type,0,witness_fun) @@ -416,7 +417,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let coq_I = Coqlib.build_coq_I () in let rec scan_type context type_of_hyp : tactic = if isLetIn type_of_hyp then - let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in + let real_type_of_hyp = Term.it_mkProd_or_LetIn type_of_hyp context in let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in (* length of context didn't change ? *) let new_context,new_typ_of_hyp = @@ -429,13 +430,13 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = then begin let (x,t_x,t') = destProd type_of_hyp in - let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in + let actual_real_type_of_hyp = Term.it_mkProd_or_LetIn t' context in if is_property ptes_infos t_x actual_real_type_of_hyp then begin let pte,pte_args = (destApp t_x) in let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar pte) ptes_infos).proving_tac in - let popped_t' = Termops.pop (EConstr.of_constr t') in - let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in + let popped_t' = pop t' in + let real_type_of_hyp = Term.it_mkProd_or_LetIn popped_t' context in let prove_new_type_of_hyp = let context_length = List.length context in tclTHENLIST @@ -486,9 +487,9 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (* observe (str "In "++Ppconstr.pr_id hyp_id++ *) (* str " removing useless precond True" *) (* ); *) - let popped_t' = Termops.pop (EConstr.of_constr t') in + let popped_t' = pop t' in let real_type_of_hyp = - it_mkProd_or_LetIn popped_t' context + Term.it_mkProd_or_LetIn popped_t' context in let prove_trivial = let nb_intro = List.length context in @@ -515,9 +516,9 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = ] else if is_trivial_eq t_x then (* t_x := t = t => we remove this precond *) - let popped_t' = Termops.pop (EConstr.of_constr t') in + let popped_t' = pop t' in let real_type_of_hyp = - it_mkProd_or_LetIn popped_t' context + Term.it_mkProd_or_LetIn popped_t' context in let hd,args = destApp t_x in let get_args hd args = @@ -616,8 +617,8 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = let fun_body = mkLambda(Anonymous, pf_unsafe_type_of g' term, - Termops.replace_term (project g') term (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info) - ) + EConstr.Unsafe.to_constr (Termops.replace_term (project g') term (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info) + )) in let new_body = pf_nf_betaiota g' (EConstr.of_constr (mkApp(fun_body,[| new_term_value |]))) in let new_body = EConstr.Unsafe.to_constr new_body in @@ -988,7 +989,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (nb_params + nb_args) t,evd in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in - let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in + let lemma_type = Term.it_mkProd_or_LetIn eqn type_ctxt in (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *) let f_id = Label.to_id (con_label (fst (destConst f))) in let prove_replacement = diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index b4eb77870..8683f68c6 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -23,6 +23,8 @@ let observe s = if do_observe () then Feedback.msg_debug s +let pop t = Vars.lift (-1) t + (* Transform an inductive induction principle into a functional one @@ -111,7 +113,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = - let res = mkApp(rel_to_fun.(i), Array.map (fun c -> Termops.pop (EConstr.of_constr c)) (array_get_start args)) in + let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); res in @@ -169,25 +171,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_env = Environ.push_rel (LocalAssum (x,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (Termops.pop (EConstr.of_constr new_b)), filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b + then (pop new_b), filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b else ( bind_fun(new_x,new_t,new_b), list_union_eq eq_constr binders_to_remove_from_t - (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b) + (List.map pop binders_to_remove_from_b) ) with | Toberemoved -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b + new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b) + new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_for_letin remove env x v t b = begin @@ -198,25 +200,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_env = Environ.push_rel (LocalDef (x,v,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (Termops.pop (EConstr.of_constr new_b)),filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b + then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b else ( mkLetIn(new_x,new_v,new_t,new_b), list_union_eq eq_constr (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) - (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b) + (List.map pop binders_to_remove_from_b) ) with | Toberemoved -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b + new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b) + new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = let new_e,to_remove_from_e = compute_new_princ_type remove env e diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index c02b64c1f..ca066c4cc 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -399,8 +399,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes match ctxt with | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") | hres::res::decl::ctxt -> - let res = Termops.it_mkLambda_or_LetIn - (Termops.it_mkProd_or_LetIn concl [hres;res]) + let res = Term.it_mkLambda_or_LetIn + (Term.it_mkProd_or_LetIn concl [hres;res]) (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt) in res @@ -793,7 +793,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( in let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; - let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in + let type_of_lemma = Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in @@ -861,7 +861,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = - Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt + Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 3688b8c15..2840193a9 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -32,7 +32,8 @@ module RelDecl = Context.Rel.Declaration (** {2 Useful operations on constr and glob_constr} *) -let rec popn i c = if i<=0 then c else EConstr.of_constr (pop (popn (i-1) c)) +let pop c = Vars.lift (-1) c +let rec popn i c = if i<=0 then c else pop (popn (i-1) c) (** Substitutions in constr *) let compare_constr_nosub t1 t2 = @@ -986,13 +987,13 @@ let relprinctype_to_funprinctype relprinctype nfuns = (* first remove indarg and indarg_in_concl *) let relinfo_noindarg = { relinfo with indarg_in_concl = false; indarg = None; - concl = EConstr.of_constr (remove_last_arg (pop relinfo.concl)); } in + concl = EConstr.of_constr (remove_last_arg (pop (EConstr.Unsafe.to_constr relinfo.concl))); } in (* the nfuns last induction arguments are functional ones: remove them *) let relinfo_argsok = { relinfo_noindarg with nargs = relinfo_noindarg.nargs - nfuns; (* args is in reverse order, so remove fst *) args = remove_n_fst_list nfuns relinfo_noindarg.args; - concl = popn nfuns relinfo_noindarg.concl; + concl = EConstr.of_constr (popn nfuns (EConstr.Unsafe.to_constr relinfo_noindarg.concl)); } in let new_branches = List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c71174fef..23b308efb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -408,6 +408,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = args.(1),args.(2) in let new_b' = Termops.replace_term (project g') (EConstr.of_constr teq_lhs) (EConstr.of_constr teq_rhs) (EConstr.of_constr new_b) in + let new_b' = EConstr.Unsafe.to_constr new_b' in let new_infos = { infos with info = new_b'; @@ -1253,7 +1254,7 @@ let clear_goals = | Prod(Name id as na,t',b) -> let b' = clear_goal b in if noccurn 1 b' && (is_rec_res id) - then Termops.pop (EConstr.of_constr b') + then Vars.lift (-1) b' else if b' == b then t else mkProd(na,t',b') | _ -> Term.map_constr clear_goal t diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 2ad97c75b..87276f5df 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -270,7 +270,7 @@ let compute_ivs f cs gl = (* The Cases predicate is a lambda; we assume no dependency *) let p = match EConstr.kind sigma p with - | Lambda (_,_,p) -> EConstr.of_constr (Termops.pop p) + | Lambda (_,_,p) -> Termops.pop p | _ -> p in diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 63eccaa40..131ecad33 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -246,7 +246,6 @@ let lapp f args = mkApp(Lazy.force f,args) let plapp evd f args = let fc = Evarutil.e_new_global evd (Lazy.force f) in - let fc = EConstr.of_constr fc in mkApp(fc,args) let dest_rel0 sigma t = @@ -591,7 +590,6 @@ let make_hyp env evd c = let make_hyp_list env evd lH = let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in - let carrier = EConstr.of_constr carrier in let l = List.fold_right (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH @@ -602,7 +600,6 @@ let make_hyp_list env evd lH = let interp_power env evd pow = let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in - let carrier = EConstr.of_constr carrier in match pow with | None -> let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in @@ -618,7 +615,6 @@ let interp_power env evd pow = let interp_sign env evd sign = let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in - let carrier = EConstr.of_constr carrier in match sign with | None -> plapp evd coq_None [|carrier|] | Some spec -> @@ -628,7 +624,6 @@ let interp_sign env evd sign = let interp_div env evd div = let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in - let carrier = EConstr.of_constr carrier in match div with | None -> plapp evd coq_None [|carrier|] | Some spec -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c0141f011..01e2db08c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1690,7 +1690,6 @@ let abstract_tycon loc env evdref subst tycon extenv t = (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in - let candidates = List.map EConstr.Unsafe.to_constr candidates in let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in lift k ev in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 87561868f..3d5a5f025 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -210,16 +210,18 @@ let computable p k = && noccur_between 1 (k+1) ccl +let pop t = Vars.lift (-1) t + let lookup_name_as_displayed env t s = let rec lookup avoid n c = match kind_of_term c with | Prod (name,_,c') -> (match compute_displayed_name_in RenamingForGoal avoid name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' - | (Anonymous,avoid') -> lookup avoid' (n+1) (pop (EConstr.of_constr c'))) + | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | LetIn (name,_,_,c') -> (match compute_displayed_name_in RenamingForGoal avoid name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' - | (Anonymous,avoid') -> lookup avoid' (n+1) (pop (EConstr.of_constr c'))) + | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | Cast (c,_,_) -> lookup avoid n c | _ -> None in lookup (ids_of_named_context (named_context env)) 1 t @@ -439,7 +441,7 @@ let detype_instance sigma l = else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) let rec detype flags avoid env sigma t = - match kind_of_term (collapse_appl sigma (EConstr.of_constr t)) with + match kind_of_term (EConstr.Unsafe.to_constr (collapse_appl sigma (EConstr.of_constr t))) with | Rel n -> (try match lookup_name_of_rel n (fst env) with | Name id -> GVar (dl, id) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9675ae2ea..6dce8627d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -147,7 +147,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then lookup_canonical_conversion (proji, Prod_cs), - (Stack.append_app [|a;EConstr.of_constr (pop b)|] Stack.empty) + (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> lookup_canonical_conversion diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 27436fdd8..3003620d7 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -189,8 +189,8 @@ let restrict_evar_key evd evk filter candidates = | None -> evar_filter evi | Some filter -> filter in let candidates = match candidates with - | NoUpdate -> evi.evar_candidates - | UpdateWith c -> Some (List.map EConstr.Unsafe.to_constr c) in + | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates + | UpdateWith c -> Some c in let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in (Sigma.to_evar_map sigma, evk) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 120adb9fe..1dcd6399e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -443,7 +443,7 @@ let build_branch_type env dep p cs = (applist (base,[build_dependent_constructor cs])) cs.cs_args else - it_mkProd_or_LetIn base cs.cs_args + Term.it_mkProd_or_LetIn base cs.cs_args (**************************************************) @@ -575,7 +575,7 @@ let arity_of_case_predicate env (ind,params) dep k = let arsign,_ = get_arity env (ind,params) in let mind = build_dependent_inductive env (ind,params) in let concl = if dep then mkArrow mind (mkSort k) else mkSort k in - it_mkProd_or_LetIn concl arsign + Term.it_mkProd_or_LetIn concl arsign (***********************************************) (* Inferring the sort of parameters of a polymorphic inductive type diff --git a/pretyping/program.ml b/pretyping/program.ml index 8ec6083f7..caa5a5c8a 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -31,7 +31,7 @@ let init_reference dir s () = coq_reference "Program" dir s let papp evdref r args = let open EConstr in let gr = delayed_force r in - mkApp (EConstr.of_constr (Evarutil.e_new_global evdref gr), args) + mkApp (Evarutil.e_new_global evdref gr, args) let sig_typ = init_reference ["Init"; "Specif"] "sig" let sig_intro = init_reference ["Init"; "Specif"] "exist" diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c796a91ca..90c5b241b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -203,10 +203,10 @@ module Cst_stack = struct let reconstruct_head = List.fold_left (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in List.fold_right - (fun (cst,params,args) t -> EConstr.of_constr (Termops.replace_term sigma + (fun (cst,params,args) t -> Termops.replace_term sigma (reconstruct_head d args) (applist (cst, List.rev params)) - t)) cst_l c + t) cst_l c let pr l = let open Pp in @@ -969,7 +969,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Rel 1, [] -> let lc = Array.sub cl 0 (napp-1) in let u = if Int.equal napp 1 then f else mkApp (f,lc) in - if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold () + if noccurn sigma 1 u then (pop u,Stack.empty),Cst_stack.empty else fold () | _ -> fold () else fold () | _ -> fold ()) @@ -1068,7 +1068,7 @@ let local_whd_state_gen flags sigma = | Rel 1, [] -> let lc = Array.sub cl 0 (napp-1) in let u = if Int.equal napp 1 then f else mkApp (f,lc) in - if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s + if noccurn sigma 1 u then (pop u,Stack.empty) else s | _ -> s else s | _ -> s) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e66d3aafe..e2c0f55f8 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -75,7 +75,7 @@ let print_ref reduce ref = if reduce then let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in let ccl = EConstr.Unsafe.to_constr ccl - in it_mkProd_or_LetIn ccl ctx + in Term.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in let env = Global.env () in diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 04f888a84..9942e911a 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -466,7 +466,7 @@ let start_proof_com ?inference_hook kind thms hook = evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, - (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), + (nf_evar !evdref (Term.it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), guard))) thms in diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 029384297..f2e98ee01 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -286,7 +286,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *) let t' = EConstr.Unsafe.to_constr t' in - match find_rel (it_mkProd_or_LetIn t' ctx) with + match find_rel (Term.it_mkProd_or_LetIn t' ctx) with | Some c -> Some c | None -> None diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3a5347bbf..b1d5d8135 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1492,7 +1492,7 @@ let _ = Used in the partial application tactic. *) let rec head_of_constr sigma t = - let t = strip_outer_cast sigma (EConstr.of_constr (collapse_appl sigma t)) in + let t = strip_outer_cast sigma (collapse_appl sigma t) in match EConstr.kind sigma t with | Prod (_,_,c2) -> head_of_constr sigma c2 | LetIn (_,_,_,c2) -> head_of_constr sigma c2 diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index a8ea7446f..e68267584 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -77,7 +77,7 @@ let build_dependent_inductive ind (mib,mip) = @ Context.Rel.to_extended_list 0 realargs) let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s -let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s +let my_it_mkProd_or_LetIn s c = Term.it_mkProd_or_LetIn c s let my_it_mkLambda_or_LetIn_name s c = it_mkLambda_or_LetIn_name (Global.env()) c s diff --git a/tactics/hints.ml b/tactics/hints.ml index 231695c35..d4b73706c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1211,7 +1211,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = | Evar (evk,args as ev) -> (* We skip the test whether args is the identity or not *) let t = existential_type sigma ev in - let t = List.fold_right (fun (e,id) c -> EConstr.of_constr (replace_term sigma e id c)) !subst t in + let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in if not (closed0 sigma c) then error "Hints with holes dependent on a bound variable not supported."; if occur_existential sigma t then @@ -1225,7 +1225,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in vars := Id.Set.add id !vars; subst := (evar,mkVar id)::!subst; - mkNamedLambda id t (iter (EConstr.of_constr (replace_term sigma evar (mkVar id) c))) in + mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in let c' = iter c in if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5ee29c089..b2f2797a6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4544,7 +4544,7 @@ let induction_gen_l isrec with_evars elim names lc = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in let id = new_fresh_id [] x gl in - let newl' = List.map (fun r -> EConstr.of_constr (replace_term sigma c (mkVar id) r)) l' in + let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in let _ = newlc:=id::!newlc in Tacticals.New.tclTHEN (letin_tac None (Name id) c None allHypsAndConcl) diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 38342b64d..219abb7fd 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -350,9 +350,11 @@ struct TDnet.Idset.fold (fun id acc -> let c_id = Opt.reduce (Ident.constr_of id) in + let c_id = EConstr.of_constr c_id in let (ctx,wc) = - try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) (EConstr.of_constr c_id) (** FIXME *) + try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) c_id (** FIXME *) with Invalid_argument _ -> [],c_id in + let wc = EConstr.Unsafe.to_constr wc in let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in try let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in diff --git a/toplevel/command.ml b/toplevel/command.ml index 1093b7fdc..820c1b885 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -118,7 +118,7 @@ let interp_definition pl bl p red_option c ctypopt = let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in let nf, subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in - let typ = nf (it_mkProd_or_LetIn ty ctx) in + let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in let beq b1 b2 = if b1 then b2 else not b2 in let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in (* Check that all implicit arguments inferable from the term @@ -583,7 +583,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = (* Interpret the arities *) let arities = List.map (interp_ind_arity env_params evdref) indl in - let fullarities = List.map (fun (c, _, _) -> it_mkProd_or_LetIn c ctx_params) arities in + let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in let env_ar = push_types env0 indnames fullarities in let env_ar_params = push_rel_context ctx_params env_ar in @@ -850,7 +850,7 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let body = interp_casted_constr_evars env evdref ~impls body ccl in it_mkLambda_or_LetIn body ctx) fix.fix_body -let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx +let build_fix_type (_,ctx) ccl = Term.it_mkProd_or_LetIn ccl ctx let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in @@ -946,7 +946,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in let top_arity = interp_type_evars top_env evdref arityc in - let full_arity = it_mkProd_or_LetIn top_arity binders_rel in + let full_arity = Term.it_mkProd_or_LetIn top_arity binders_rel in let argtyp, letbinders, make = telescope binders_rel in let argname = Id.of_string "recarg" in let arg = LocalAssum (Name argname, argtyp) in @@ -998,7 +998,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let intern_arity = substl [projection] top_arity_let in (* substitute the projection of wfarg for something, now intern_arity is in wfarg :: arg *) - let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in + let intern_fun_arity_prod = Term.it_mkProd_or_LetIn intern_arity [wfarg 1] in let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in let curry_fun = let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in @@ -1008,7 +1008,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let rcurry = mkApp (rel, [| measure; lift len measure |]) in let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in - let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in + let ty = Term.it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in LocalDef (Name recname, body, ty) in let fun_bl = intern_fun_binder :: [arg] in @@ -1045,7 +1045,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let name = add_suffix recname "_func" in let hook l gr _ = let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in - let ty = it_mkProd_or_LetIn top_arity binders_rel in + let ty = Term.it_mkProd_or_LetIn top_arity binders_rel in let pl, univs = Evd.universe_context ?names:pl !evdref in (*FIXME poly? *) let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in @@ -1055,10 +1055,10 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in - let typ = it_mkProd_or_LetIn top_arity binders in + let typ = Term.it_mkProd_or_LetIn top_arity binders in hook, name, typ else - let typ = it_mkProd_or_LetIn top_arity binders_rel in + let typ = Term.it_mkProd_or_LetIn top_arity binders_rel in let hook l gr _ = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 2a0ebf402..6da2f82ab 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -142,10 +142,11 @@ let trunc_named_context n ctx = List.firstn (len - n) ctx let rec chop_product n t = + let pop t = Vars.lift (-1) t in 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 (EConstr.of_constr b)) else None + | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None | _ -> None let evar_dependencies evm oev = diff --git a/toplevel/record.ml b/toplevel/record.ml index 96221b742..73035deb0 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -375,7 +375,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 evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t)) decl) 1 tl in + RelDecl.map_type (fun t -> EConstr.Unsafe.to_constr (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) |