diff options
37 files changed, 106 insertions, 127 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index ecc6ab68e..abaa409bd 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -276,10 +276,11 @@ let last_arg sigma c = match EConstr.kind sigma c with (* Get the last arg of an application *) let decompose_app_vect sigma c = match EConstr.kind sigma c with - | App (f,cl) -> (EConstr.Unsafe.to_constr f, Array.map EConstr.Unsafe.to_constr cl) - | _ -> (EConstr.Unsafe.to_constr c,[||]) + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) let adjust_app_list_size f1 l1 f2 l2 = + let open EConstr in let len1 = List.length l1 and len2 = List.length l2 in if Int.equal len1 len2 then (f1,l1,f2,l2) else if len1 < len2 then @@ -698,13 +699,13 @@ let rec subst_meta bl c = let rec strip_outer_cast sigma c = match EConstr.kind sigma c with | Cast (c,_,_) -> strip_outer_cast sigma c - | _ -> EConstr.Unsafe.to_constr c + | _ -> c (* flattens application lists throwing casts in-between *) let collapse_appl sigma c = match EConstr.kind sigma c with | App (f,cl) -> let rec collapse_rec f cl2 = - match EConstr.kind sigma (EConstr.of_constr (strip_outer_cast sigma f)) with + match EConstr.kind sigma (strip_outer_cast sigma f) with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | _ -> EConstr.mkApp (f,cl2) in @@ -744,15 +745,17 @@ let my_prefix_application sigma eq_fun (k,c) by_c t = works if [c] has rels *) let subst_term_gen sigma eq_fun c t = + let open EConstr in + let open Vars in let rec substrec (k,c as kc) t = match prefix_application sigma eq_fun kc t with | Some x -> x | None -> if eq_fun sigma c t then EConstr.mkRel k else - EConstr.map_with_binders sigma (fun (k,c) -> (k+1, EConstr.Vars.lift 1 c)) substrec kc t + EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t in - EConstr.Unsafe.to_constr (substrec (1,c) t) + substrec (1,c) t let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c t diff --git a/engine/termops.mli b/engine/termops.mli index 05604beda..426b5f34d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -144,7 +144,7 @@ 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 -> constr + (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> EConstr.constr (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] as equality *) @@ -153,7 +153,7 @@ val replace_term_gen : EConstr.t -> EConstr.t -> EConstr.t -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) -val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> constr +val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.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 @@ -174,7 +174,7 @@ val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t (** 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 -> constr +val strip_outer_cast : Evd.evar_map -> EConstr.t -> EConstr.constr exception CannotFilter @@ -204,10 +204,10 @@ val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr (** Force the decomposition of a term as an applicative one *) -val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array +val decompose_app_vect : Evd.evar_map -> EConstr.t -> 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_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) diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index ecb653587..119e872f8 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -323,7 +323,7 @@ end) = struct | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f -> decomp_pointwise sigma (pred n) relb | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f -> - decomp_pointwise sigma (pred n) (EConstr.of_constr (Reductionops.beta_applist sigma (arelb, [mkRel 1]))) + decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1])) | _ -> invalid_arg "decomp_pointwise" let rec apply_pointwise sigma rel = function @@ -332,7 +332,7 @@ end) = struct | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f -> apply_pointwise sigma relb args | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f -> - apply_pointwise sigma (EConstr.of_constr (Reductionops.beta_applist sigma (arelb, [arg]))) args + apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args | _ -> invalid_arg "apply_pointwise") | [] -> rel @@ -1000,7 +1000,6 @@ let fold_match ?(force=false) env sigma c = in let app = let ind, args = Inductiveops.find_mrectype env sigma cty in - let args = List.map EConstr.of_constr args in let pars, args = List.chop ci.ci_npar args in let meths = List.map (fun br -> br) (Array.to_list brs) in applist (mkConst sk, pars @ [pred] @ meths @ args @ [c]) diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 27398cf65..4d2859fb0 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -15,7 +15,7 @@ let get_inductive dir s = Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) let decomp_term sigma (c : Term.constr) = - Term.kind_of_term (Termops.strip_outer_cast sigma (EConstr.of_constr c)) + Term.kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) let lapp c v = Term.mkApp (Lazy.force c, v) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index a12ef00ec..6295e004e 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -87,6 +87,7 @@ let rec decompose_term env sigma t= (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) | _ -> let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in + let t = EConstr.Unsafe.to_constr t in if closed0 t then Symb t else raise Not_found (* decompose equality in members and type *) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 5de2c4151..e73166be2 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -786,7 +786,7 @@ let rec consider_match may_intro introduced available expected gls = let consider_tac c hyps gls = let c = EConstr.of_constr c in - match kind_of_term (strip_outer_cast (project gls) c) with + match EConstr.kind (project gls) (strip_outer_cast (project gls) c) with Var id -> consider_match false [] [id] hyps gls | _ -> @@ -811,6 +811,9 @@ let rec take_tac wits gls = (* tactics for define *) +let subst_term sigma c t = + EConstr.Unsafe.to_constr (subst_term sigma c t) + let rec build_function sigma args body = match args with st::rest -> diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index e9fd40722..460157130 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,11 +42,11 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) + Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) let sort_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) (*S Generation of flags and signatures. *) diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index fb237f29b..205cb282d 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -21,7 +21,8 @@ exception UFAIL of constr*constr to the equation set. Raises UFAIL with a pair of terms *) -let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *) +let strip_outer_cast t = + EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *) let unif t1 t2= let evd = Evd.empty in (** FIXME *) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index dbb5cc2de..f9802ee5e 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -471,6 +471,7 @@ let rec fourier () = let sigma = Tacmach.New.project gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in + let goal = EConstr.Unsafe.to_constr goal in let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 09e77598a..04a747fb4 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -183,7 +183,7 @@ type inversion_scheme = { let i_can't_do_that () = error "Quote: not a simple fixpoint" -let decomp_term gl c = kind_of_term (Termops.strip_outer_cast (Tacmach.New.project gl) (EConstr.of_constr c)) +let decomp_term gl c = kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast (Tacmach.New.project gl) (EConstr.of_constr c))) (*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ... ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 119e92c82..76ced2b1d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2335,7 +2335,7 @@ let abstract_tomatch env sigma tomatchs tycon = Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon | _ -> let tycon = Option.map - (fun t -> EConstr.of_constr (subst_term sigma (lift 1 c) (lift 1 t))) tycon in + (fun t -> subst_term sigma (lift 1 c) (lift 1 t)) tycon in let name = next_ident_away (Id.of_string "filtered_var") names in (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, local_def (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index d67976232..48f7be4bb 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -502,8 +502,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in let t2 = match v2 with | None -> subst_term evd' v1 t2 - | Some v2 -> Retyping.get_type_of env1 evd' (EConstr.of_constr v2) in - let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly (Option.map EConstr.of_constr v2) (EConstr.of_constr t2) u2 in + | Some v2 -> EConstr.of_constr (Retyping.get_type_of env1 evd' v2) in + let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 06daa5116..55612aa66 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -185,7 +185,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels else false) in let rec sorec ctx env subst p t = - let cT = EConstr.of_constr (strip_outer_cast sigma t) in + let cT = strip_outer_cast sigma t in match p, EConstr.kind sigma cT with | PSoApp (n,args),m -> let fold (ans, seen) = function diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c0611dcec..87561868f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -267,7 +267,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = | [] -> (List.rev nal,(e,c)) | b::tags -> let na,c,f,body,t = - match kind_of_term (strip_outer_cast sigma (EConstr.of_constr c)), b with + match kind_of_term (EConstr.Unsafe.to_constr (strip_outer_cast sigma (EConstr.of_constr c))), b with | Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t | LetIn (na,b,t,c),true -> na,c,compute_displayed_name_in,Some b,Some t @@ -503,6 +503,7 @@ let rec detype flags avoid env sigma t = let body = pb.Declarations.proj_body in let ty = Retyping.get_type_of (snd env) sigma (EConstr.of_constr c) in let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma (EConstr.of_constr ty) in + let args = List.map EConstr.Unsafe.to_constr args in let body' = strip_lam_assum body in let body' = subst_instance_constr u body' in substl (c :: List.rev args) body' diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a968af7ff..9675ae2ea 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -170,7 +170,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let (i,u), ind_args = try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) with _ -> raise Not_found - in Stack.append_app_list (List.map EConstr.of_constr ind_args) Stack.empty, c, sk1 + in Stack.append_app_list ind_args Stack.empty, c, sk1 | None -> match Stack.strip_n_app nparams sk1 with | Some (params1, c1, extra_args1) -> params1, c1, extra_args1 @@ -188,7 +188,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let t' = subst_univs_level_constr subst t' in let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in let h, _ = decompose_app_vect sigma t' in - ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), + ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, (n, Stack.zip sigma (t2,sk2)) @@ -907,7 +907,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); test; (fun i -> evar_conv_x trs env i CONV h2 - (EConstr.of_constr (fst (decompose_app_vect i (substl ks h)))))] + (fst (decompose_app_vect i (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 772571926..65b6d287d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -518,7 +518,6 @@ let is_unification_pattern (env,nb) evd f l t = let solve_pattern_eqn env sigma l c = let c' = List.fold_right (fun a c -> let c' = subst_term sigma (lift 1 a) (lift 1 c) in - let c' = EConstr.of_constr c' in match EConstr.kind sigma a with (* Rem: if [a] links to a let-in, do as if it were an assumption *) | Rel n -> @@ -557,7 +556,7 @@ let make_projectable_subst aliases sigma evi args = | LocalAssum (id,c), a::rest -> let cstrs = let a',args = decompose_app_vect sigma a in - match EConstr.kind sigma (EConstr.of_constr a') with + match EConstr.kind sigma a' with | Construct cstr -> let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in Constrmap.add (fst cstr) ((args,id)::l) cstrs @@ -691,7 +690,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst = List.filter (fun (args',id) -> (* is_conv is maybe too strong (and source of useless computation) *) (* (at least expansion of aliases is needed) *) - Array.for_all2 (fun c1 c2 -> is_conv env evd c1 (EConstr.of_constr c2)) args args') l in + Array.for_all2 (fun c1 c2 -> is_conv env evd c1 c2) args args') l in List.map snd l with Not_found -> [] @@ -1104,14 +1103,14 @@ exception CannotProject of evar_map * EConstr.existential let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t = let f,args = decompose_app_vect evd t in - match EConstr.kind evd (EConstr.of_constr f) with + match EConstr.kind evd f with | Construct ((ind,_),u) -> let n = Inductiveops.inductive_nparams ind in if n > Array.length args then true (* We don't try to be more clever *) else let params = fst (Array.chop n args) in - Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) params - | Ind _ -> Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) args + Array.for_all (is_constrainable_in false evd k g) params + | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2 | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids @@ -1463,8 +1462,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = progress := true; match let c,args = decompose_app_vect !evdref t in - let args = Array.map EConstr.of_constr args in - match EConstr.kind !evdref (EConstr.of_constr c) with + match EConstr.kind !evdref c with | Construct (cstr,u) when noccur_between !evdref 1 k t -> (* This is common case when inferring the return clause of match *) (* (currently rudimentary: we do not treat the case of multiple *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index cb8b25323..9c5a2e894 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -451,13 +451,13 @@ let extract_mrectype sigma t = let open EConstr in let (t, l) = decompose_app sigma t in match EConstr.kind sigma t with - | Ind ind -> (ind, List.map EConstr.Unsafe.to_constr l) + | Ind ind -> (ind, l) | _ -> raise Not_found let find_mrectype_vect env sigma c = let open EConstr in let (t, l) = Termops.decompose_app_vect sigma (EConstr.of_constr (whd_all env sigma c)) in - match EConstr.kind sigma (EConstr.of_constr t) with + match EConstr.kind sigma t with | Ind ind -> (ind, l) | _ -> raise Not_found diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1614e1817..4bb484759 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -161,9 +161,9 @@ val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) -val extract_mrectype : evar_map -> EConstr.t -> pinductive * constr list -val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * constr list -val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * constr array +val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list +val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr list +val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr array val find_rectype : env -> evar_map -> EConstr.types -> inductive_type val find_inductive : env -> evar_map -> EConstr.types -> pinductive * constr list val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * constr list diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c792bf2ca..f814028f9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -971,7 +971,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in - let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[cj.uj_val]))) in + let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in pred, typ | None -> let p = match tycon with @@ -987,7 +987,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let n = Context.Rel.length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in - let pi = EConstr.of_constr pi in let csgn = if not !allow_anonymous_refs then List.map (set_name Anonymous) cs.cs_args diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 31354217f..6ec3cd985 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -669,7 +669,7 @@ let beta_app sigma (c,l) = let beta_applist sigma (c,l) = let zip s = Stack.zip sigma s in - EConstr.Unsafe.to_constr (stacklam zip [] sigma c (Stack.append_app_list l Stack.empty)) + stacklam zip [] sigma c (Stack.append_app_list l Stack.empty) (* Iota reduction tools *) @@ -1611,8 +1611,8 @@ let meta_reducible_instance evd b = let u = whd_betaiota Evd.empty u (** FIXME *) in let u = EConstr.of_constr u in match EConstr.kind evd u with - | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd c)) -> - let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd c)) in + | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> + let m = destMeta evd (strip_outer_cast evd c) in (match try let g, s = Metamap.find m metas in @@ -1623,8 +1623,8 @@ let meta_reducible_instance evd b = with | Some g -> irec (mkCase (ci,p,g,bl)) | None -> mkCase (ci,irec p,c,Array.map irec bl)) - | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd f)) -> - let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd f)) in + | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) -> + let m = destMeta evd (strip_outer_cast evd f) in (match try let g, s = Metamap.find m metas in @@ -1671,8 +1671,8 @@ let head_unfold_under_prod ts env sigma c = | Prod (n,t,c) -> mkProd (n,aux t, aux c) | _ -> let (h,l) = decompose_app_vect sigma c in - match EConstr.kind sigma (EConstr.of_constr h) with - | Const cst -> beta_app sigma (unfold cst, Array.map EConstr.of_constr l) + match EConstr.kind sigma h with + | Const cst -> beta_app sigma (unfold cst, l) | _ -> c in EConstr.Unsafe.to_constr (aux c) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1e6527b29..3b3242537 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -204,7 +204,7 @@ val shrink_eta : EConstr.constr -> EConstr.constr val safe_evar_value : evar_map -> existential -> constr option -val beta_applist : evar_map -> EConstr.t * EConstr.t list -> constr +val beta_applist : evar_map -> EConstr.t * EConstr.t list -> EConstr.constr val hnf_prod_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr val hnf_prod_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 88899e633..3142ea5cb 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -59,7 +59,7 @@ let local_def (na, b, t) = LocalDef (na, inj b, inj t) let get_type_from_constraints env sigma t = - if isEvar sigma (EConstr.of_constr (fst (decompose_app_vect sigma t))) then + if isEvar sigma (fst (decompose_app_vect sigma t)) then match List.map_filter (fun (pbty,env,t1,t2) -> if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2 @@ -102,7 +102,7 @@ let retype ?(polyprop=true) sigma = let rec type_of env cstr = match EConstr.kind sigma cstr with | Meta n -> - EConstr.of_constr (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) + (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) with Not_found -> retype_error (BadMeta n)) | Rel n -> let ty = EConstr.of_constr (RelDecl.get_type (lookup_rel n env)) in @@ -135,10 +135,10 @@ let retype ?(polyprop=true) sigma = | CoFix (i,(_,tys,_)) -> tys.(i) | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in - EConstr.of_constr (strip_outer_cast sigma (subst_type env sigma t (Array.to_list args))) + strip_outer_cast sigma (subst_type env sigma t (Array.to_list args)) | App(f,args) -> - EConstr.of_constr (strip_outer_cast sigma - (subst_type env sigma (type_of env f) (Array.to_list args))) + strip_outer_cast sigma + (subst_type env sigma (type_of env f) (Array.to_list args)) | Proj (p,c) -> let ty = type_of env c in EConstr.of_constr (try @@ -259,6 +259,5 @@ let expand_projection env sigma pr c args = try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) with Not_found -> retype_error BadRecursiveType in - let ind_args = List.map EConstr.of_constr ind_args in mkApp (mkConstU (Projection.constant pr,u), Array.of_list (ind_args @ (c :: args))) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1ec8deb1b..1d179c683 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -427,8 +427,6 @@ let solve_arity_problem env sigma fxminargs c = let rec check strict c = let c' = EConstr.of_constr (whd_betaiotazeta sigma c) in let (h,rcargs) = decompose_app_vect sigma c' in - let rcargs = Array.map EConstr.of_constr rcargs in - let h = EConstr.of_constr h in match EConstr.kind sigma h with Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) -> let minargs = Evar.Map.find i fxminargs in @@ -734,14 +732,13 @@ and reduce_params env sigma stack l = and whd_simpl_stack env sigma = let rec redrec s = let (x, stack) = decompose_app_vect sigma s in - let stack = Array.map_to_list EConstr.of_constr stack in - let x = EConstr.of_constr x in + let stack = Array.to_list stack in let s' = (x, stack) in match EConstr.kind sigma x with | Lambda (na,t,c) -> (match stack with | [] -> s' - | a :: rest -> redrec (EConstr.of_constr (beta_applist sigma (x, stack)))) + | a :: rest -> redrec (beta_applist sigma (x, stack))) | LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack)) | App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack)) | Cast (c,_,_) -> redrec (applist(c, stack)) @@ -1122,14 +1119,12 @@ let fold_one_com com env sigma c = unfold produces it, so that the "unfold f; fold f" configuration works to refold fix expressions *) let a = subst_term sigma (EConstr.of_constr (clos_norm_flags unfold_side_red env sigma rcom)) c in - let a = EConstr.of_constr a in if not (EConstr.eq_constr sigma a c) then Vars.subst1 com a else (* Then reason on the non beta-iota-zeta form for compatibility - even if it is probably a useless configuration *) let a = subst_term sigma rcom c in - let a = EConstr.of_constr a in Vars.subst1 com a let fold_commands cl env sigma c = @@ -1195,7 +1190,7 @@ let reduce_to_ind_gen allow_product env sigma t = let rec elimrec env t l = let t = hnf_constr env sigma t in let t = EConstr.of_constr t in - match EConstr.kind sigma (EConstr.of_constr (fst (decompose_app_vect sigma t))) with + match EConstr.kind sigma (fst (decompose_app_vect sigma t)) with | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l) | Prod (n,ty,t') -> let open Context.Rel.Declaration in @@ -1208,7 +1203,7 @@ let reduce_to_ind_gen allow_product env sigma t = was partially the case between V5.10 and V8.1 *) let t' = whd_all env sigma t in let t' = EConstr.of_constr t' in - match EConstr.kind sigma (EConstr.of_constr (fst (decompose_app_vect sigma t'))) with + match EConstr.kind sigma (fst (decompose_app_vect sigma t')) with | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l) | _ -> user_err (str"Not an inductive product.") in @@ -1275,7 +1270,6 @@ let reduce_to_ref_gen allow_product env sigma ref t = (* lazily reduces to match the head of [t] with the expected [ref] *) let rec elimrec env t l = let c, _ = decompose_app_vect sigma t in - let c = EConstr.of_constr c in match EConstr.kind sigma c with | Prod (n,ty,t') -> if allow_product then diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index a970c434f..f59a6dcd9 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -156,17 +156,17 @@ let class_of_constr sigma c = try Some (dest_class_arity (Global.env ()) sigma c) with e when CErrors.noncritical e -> None -let is_class_constr c = - try let gr, u = Universes.global_of_constr c in +let is_class_constr sigma c = + try let gr, u = Termops.global_of_constr sigma c in Refmap.mem gr !classes with Not_found -> false let rec is_class_type evd c = let c, _ = Termops.decompose_app_vect evd c in - match EConstr.kind evd (EConstr.of_constr c) with + match EConstr.kind evd c with | Prod (_, _, t) -> is_class_type evd t | Cast (t, _, _) -> is_class_type evd t - | _ -> is_class_constr c + | _ -> is_class_constr evd c let is_class_evar evd evi = is_class_type evd (EConstr.of_constr evi.Evd.evar_concl) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 29697260f..40ef2450a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -138,7 +138,7 @@ let e_type_case_branches env evdref (ind,largs) pj c = let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in - let realargs = List.map EConstr.of_constr realargs in + let params = List.map EConstr.Unsafe.to_constr params in let () = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in let lc = Array.map EConstr.of_constr lc in @@ -232,7 +232,6 @@ let judge_of_projection env sigma p cj = try find_mrectype env sigma cj.uj_type with Not_found -> error_case_not_inductive env sigma cj in - let args = List.map EConstr.of_constr args in let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in let ty = substl (cj.uj_val :: List.rev args) ty in {uj_val = EConstr.mkProj (p,cj.uj_val); diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 81d9ecad5..169dd45bc 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -632,7 +632,7 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM let rec is_neutral env sigma ts t = let (f, l) = decompose_app_vect sigma t in - match EConstr.kind sigma (EConstr.of_constr f) with + match EConstr.kind sigma f with | Const (c, u) -> not (Environ.evaluable_constant c env) || not (is_transparent env (ConstKey c)) || @@ -1488,10 +1488,6 @@ let w_unify_core_0 env evd with_types cv_pb flags m n = let w_typed_unify env evd = w_unify_core_0 env evd true let w_typed_unify_array env evd flags f1 l1 f2 l2 = - let f1 = EConstr.of_constr f1 in - let f2 = EConstr.of_constr f2 in - let l1 = Array.map EConstr.of_constr l1 in - let l2 = Array.map EConstr.of_constr l2 in let f1,l1,f2,l2 = adjust_app_array_size f1 l1 f2 l2 in let (mc1,evd') = retract_coercible_metas evd in let fold_subst subst m n = unify_0_with_initial_metas subst true env CONV flags.core_unify_flags m n in @@ -1743,7 +1739,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = let bestexn = ref None in let kop = Keys.constr_key (EConstr.to_constr evd op) in let rec matchrec cl = - let cl = EConstr.of_constr (strip_outer_cast evd cl) in + let cl = strip_outer_cast evd cl in (try if closed0 evd cl && not (isEvar evd cl) && keyed_unify env evd kop cl then (try @@ -1837,7 +1833,6 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = in let rec matchrec cl = let cl = strip_outer_cast evd cl in - let cl = EConstr.of_constr cl in (bind (if closed0 evd cl then return (fun () -> w_typed_unify env evd CONV flags op cl,cl) @@ -1898,7 +1893,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = unify pre-existing non frozen evars of the goal or of the pattern *) set_no_delta_flags flags in - let t' = (EConstr.of_constr (strip_outer_cast evd op),t) in + let t' = (strip_outer_cast evd op,t) in let (evd',cl) = try if is_keyed_unification () then @@ -1992,7 +1987,7 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = let hd2,l2 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty2)) in let is_empty1 = Array.is_empty l1 in let is_empty2 = Array.is_empty l2 in - match kind_of_term hd1, not is_empty1, kind_of_term hd2, not is_empty2 with + match EConstr.kind evd hd1, not is_empty1, EConstr.kind evd hd2, not is_empty2 with (* Pattern case *) | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) when Int.equal (Array.length l1) (Array.length l2) -> diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d98669660..572db1d40 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -266,7 +266,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = let concl = Goal.V82.concl clenv.evd (sig_it gl) in - if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus))))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus)))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) else @@ -480,7 +480,7 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u))))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u)))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 539b1bcb2..84cdc09ee 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -34,7 +34,7 @@ let clenv_cast_meta clenv = | _ -> EConstr.map clenv.evd crec u and crec_hd u = - match EConstr.kind clenv.evd (EConstr.of_constr (strip_outer_cast clenv.evd u)) with + match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with | Meta mv -> (try let b = Typing.meta_type clenv.evd mv in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 0ca661557..6c45bef1c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1496,7 +1496,6 @@ let _ = let rec head_of_constr sigma t = let t = strip_outer_cast sigma (EConstr.of_constr (collapse_appl sigma t)) in - let t = EConstr.of_constr 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/equality.ml b/tactics/equality.ml index 4c79a6199..2eead2d22 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -183,7 +183,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = w_unify_to_subterm_all ~flags env eqclause.evd - (EConstr.of_constr (if l2r then c1 else c2),EConstr.of_constr concl) + ((if l2r then c1 else c2),concl) in List.map try_occ occs let instantiate_lemma gl c ty l l2r concl = @@ -314,6 +314,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = | None -> pf_nf_concl gl | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl) in + let typ = EConstr.of_constr typ in let cs = instantiate_lemma typ in if firstonly then tclFIRST (List.map try_clause cs) else tclMAP try_clause cs @@ -1207,7 +1208,6 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in let ev = Evarutil.e_new_evar env evdref a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in - let rty = EConstr.of_constr rty in let tuple_tail = sigrec_clausal_form (siglen-1) rty in let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in match evopt with @@ -1348,10 +1348,6 @@ let inject_if_homogenous_dependent_pair ty = if not (Termops.is_global sigma (sigTconstr()) eqTypeDest) then raise Exit; let hd1,ar1 = decompose_app_vect sigma t1 and hd2,ar2 = decompose_app_vect sigma t2 in - let hd1 = EConstr.of_constr hd1 in - let hd2 = EConstr.of_constr hd2 in - let ar1 = Array.map EConstr.of_constr ar1 in - let ar2 = Array.map EConstr.of_constr ar2 in if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit; if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit; let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in @@ -1565,7 +1561,6 @@ let decomp_tuple_term env sigma c t = let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code]) and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in let cdrtyp = beta_applist sigma (p,[car]) in - let cdrtyp = EConstr.of_constr cdrtyp in List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp) with Constr_matching.PatternMatchingFailure -> [] @@ -1593,13 +1588,11 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* We build the expected goal *) let abst_B = List.fold_right - (fun (e,t) body -> lambda_create env (t,EConstr.of_constr (subst_term sigma e body))) e1_list b in + (fun (e,t) body -> lambda_create env (t,subst_term sigma e body)) e1_list b in let pred_body = beta_applist sigma (abst_B,proj_list) in - let pred_body = EConstr.of_constr pred_body in let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in (* Simulate now the normalisation treatment made by Logic.mk_refgoals *) - let expected_goal = EConstr.of_constr expected_goal in let expected_goal = nf_betaiota sigma expected_goal in let expected_goal = EConstr.of_constr expected_goal in (* Retype to get universes right *) diff --git a/tactics/hints.ml b/tactics/hints.ml index cd5fc79f5..2b310033c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -50,7 +50,6 @@ exception Bound let head_constr_bound sigma t = let t = strip_outer_cast sigma t in - let t = EConstr.of_constr t in let _,ccl = decompose_prod_assum sigma t in let hd,args = decompose_app sigma ccl in match EConstr.kind sigma hd with @@ -66,11 +65,8 @@ let head_constr sigma c = let decompose_app_bound sigma t = let t = strip_outer_cast sigma t in - let t = EConstr.of_constr t in let _,ccl = decompose_prod_assum sigma t in let hd,args = decompose_app_vect sigma ccl in - let hd = EConstr.of_constr hd in - let args = Array.map EConstr.of_constr args in match EConstr.kind sigma hd with | Const (c,u) -> ConstRef c, args | Ind (i,u) -> IndRef i, args @@ -754,7 +750,6 @@ let secvars_of_global env gr = let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = let secvars = secvars_of_constr env sigma c in let cty = strip_outer_cast sigma cty in - let cty = EConstr.of_constr cty in match EConstr.kind sigma cty with | Prod _ -> failwith "make_exact_entry" | _ -> diff --git a/tactics/inv.ml b/tactics/inv.ml index 5c296b343..ac9a564e5 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -462,7 +462,6 @@ let raw_inversion inv_kind id status names = Reductionops.beta_applist sigma (elim_predicate, realargs), case_nodep_then_using in - let cut_concl = EConstr.of_constr cut_concl in let refined id = let prf = mkApp (mkVar id, args) in Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) } diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 606eb27b9..03f81773b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -528,7 +528,7 @@ fun env sigma p -> function let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in Sigma (arg :: rem, sigma, r) -let rec check_mutind env sigma k cl = match EConstr.kind sigma (EConstr.of_constr (strip_outer_cast sigma cl)) with +let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast sigma cl) with | Prod (na, c1, b) -> if Int.equal k 1 then try @@ -1647,10 +1647,8 @@ let make_projection env sigma params cstr sign elim i n c u = then let t = lift (i+1-n) t in let abselim = beta_applist sigma (elim, params@[t;branch]) in - let abselim = EConstr.of_constr abselim in let args = Array.map EConstr.of_constr (Context.Rel.to_extended_vect 0 sign) in let c = beta_applist sigma (abselim, [mkApp (c, args)]) in - let c = EConstr.of_constr c in Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign) else None @@ -2856,7 +2854,7 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let open Context.Rel.Declaration in let decls,cl = decompose_prod_n_assum sigma i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in - let newdecls,_ = decompose_prod_n_assum sigma i (EConstr.of_constr (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod)) in + let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in let cl' = EConstr.of_constr cl' in let na = generalized_name sigma c t ids cl' na in diff --git a/toplevel/class.ml b/toplevel/class.ml index 6788cf1b7..e55489471 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -81,12 +81,13 @@ let check_target clt = function (* condition d'heritage uniforme *) -let uniform_cond nargs lt = +let uniform_cond sigma nargs lt = + let open EConstr in let rec aux = function | (0,[]) -> true | (n,t::l) -> - let t = strip_outer_cast Evd.empty t (** FIXME *) in - isRel t && Int.equal (destRel t) n && aux ((n-1),l) + let t = strip_outer_cast sigma t in + isRel sigma t && Int.equal (destRel sigma t) n && aux ((n-1),l) | _ -> false in aux (nargs,lt) @@ -263,7 +264,7 @@ let add_new_coercion_core coef stre poly source target isid = raise (CoercionError (NoSource source)) in check_source (Some cls); - if not (uniform_cond (llp-ind) lvs) then + if not (uniform_cond Evd.empty (** FIXME *) (llp-ind) lvs) then warn_uniform_inheritance coef; let clt = try diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 8aee9d241..aac1d1ed4 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -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 Evd.empty (EConstr.of_constr t)) (** FIXME *) with + match kind_of_term (EConstr.Unsafe.to_constr (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 | _ -> diff --git a/toplevel/search.ml b/toplevel/search.ml index 653d4ac5c..102bd003d 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -111,20 +111,20 @@ 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 Evd.empty (EConstr.of_constr typ) (** FIXME *) in - if Constr_matching.is_matching env Evd.empty pat (EConstr.of_constr typ) then true - else match kind_of_term typ with +let rec pattern_filter pat ref env sigma typ = + let typ = Termops.strip_outer_cast sigma typ in + if Constr_matching.is_matching env sigma pat typ then true + else match EConstr.kind sigma typ with | Prod (_, _, typ) - | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ + | LetIn (_, _, _, typ) -> pattern_filter pat ref env sigma typ | _ -> false -let rec head_filter pat ref env typ = - let typ = Termops.strip_outer_cast Evd.empty (EConstr.of_constr typ) (** FIXME *) in - if Constr_matching.is_matching_head env Evd.empty pat (EConstr.of_constr typ) then true - else match kind_of_term typ with +let rec head_filter pat ref env sigma typ = + let typ = Termops.strip_outer_cast sigma typ in + if Constr_matching.is_matching_head env sigma pat typ then true + else match EConstr.kind sigma typ with | Prod (_, _, typ) - | LetIn (_, _, _, typ) -> head_filter pat ref env typ + | LetIn (_, _, _, typ) -> head_filter pat ref env sigma typ | _ -> false let full_name_of_reference ref = @@ -162,7 +162,7 @@ let search_pattern gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && - pattern_filter pat ref env typ && + pattern_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) && blacklist_filter ref env typ in let iter ref env typ = @@ -186,8 +186,8 @@ let search_rewrite gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && - (pattern_filter pat1 ref env typ || - pattern_filter pat2 ref env typ) && + (pattern_filter pat1 ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) || + pattern_filter pat2 ref env Evd.empty (EConstr.of_constr typ)) && blacklist_filter ref env typ in let iter ref env typ = @@ -201,7 +201,7 @@ let search_by_head gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && - head_filter pat ref env typ && + head_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) && blacklist_filter ref env typ in let iter ref env typ = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3b8c62738..773766d7e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -103,11 +103,12 @@ let try_print_subgoals () = (* Simulate the Intro(s) tactic *) let show_intro all = + let open EConstr in let pf = get_pftreestate() in 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 (project gl) (EConstr.of_constr (pf_concl gl))) in + let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (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)) |