diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 16:18:47 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
commit | b4b90c5d2e8c413e1981c456c933f35679386f09 (patch) | |
tree | fc84ec244390beb2f495b024620af2e130ad5852 | |
parent | 78a8d59b39dfcb07b94721fdcfd9241d404905d2 (diff) |
Definining EConstr-based contexts.
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
79 files changed, 759 insertions, 816 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 629be8e4b..657285de2 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -77,6 +77,10 @@ type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint type unsafe_judgment = (constr, types) Environ.punsafe_judgment type unsafe_type_judgment = types Environ.punsafe_type_judgment +type named_declaration = (constr, types) Context.Named.Declaration.pt +type rel_declaration = (constr, types) Context.Rel.Declaration.pt +type named_context = (constr, types) Context.Named.pt +type rel_context = (constr, types) Context.Rel.pt let in_punivs a = (a, Univ.Instance.empty) @@ -201,14 +205,6 @@ let decompose_app sigma c = | App (f,cl) -> (f, Array.to_list cl) | _ -> (c,[]) -let local_assum (na, t) = - let open Rel.Declaration in - LocalAssum (na, unsafe_to_constr t) - -let local_def (na, b, t) = - let open Rel.Declaration in - LocalDef (na, unsafe_to_constr b, unsafe_to_constr t) - let decompose_lam sigma c = let rec lamdec_rec l c = match kind sigma c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c @@ -218,38 +214,41 @@ let decompose_lam sigma c = lamdec_rec [] c let decompose_lam_assum sigma c = + let open Rel.Declaration in let rec lamdec_rec l c = match kind sigma c with - | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) c - | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) c + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in lamdec_rec Context.Rel.empty c let decompose_lam_n_assum sigma n c = + let open Rel.Declaration in if n < 0 then error "decompose_lam_n_assum: integer parameter must be positive"; let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match kind sigma c with - | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) n c + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_assum: not enough abstractions" in lamdec_rec Context.Rel.empty n c let decompose_lam_n_decls sigma n = + let open Rel.Declaration in if n < 0 then error "decompose_lam_n_decls: integer parameter must be positive"; let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match kind sigma c with - | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_decls: not enough abstractions" in @@ -264,24 +263,26 @@ let decompose_prod sigma c = proddec_rec [] c let decompose_prod_assum sigma c = + let open Rel.Declaration in let rec proddec_rec l c = match kind sigma c with - | Prod (x,t,c) -> proddec_rec (Context.Rel.add (local_assum (x,t)) l) c - | LetIn (x,b,t,c) -> proddec_rec (Context.Rel.add (local_def (x,b,t)) l) c + | Prod (x,t,c) -> proddec_rec (Context.Rel.add (LocalAssum (x,t)) l) c + | LetIn (x,b,t,c) -> proddec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> proddec_rec l c | _ -> l,c in proddec_rec Context.Rel.empty c let decompose_prod_n_assum sigma n c = + let open Rel.Declaration in if n < 0 then error "decompose_prod_n_assum: integer parameter must be positive"; let rec prodec_rec l n c = if Int.equal n 0 then l,c else match kind sigma c with - | Prod (x,t,c) -> prodec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c - | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c + | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c + | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | c -> error "decompose_prod_n_assum: not enough assumptions" in @@ -413,24 +414,26 @@ let iter sigma f c = match kind sigma c with | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl -let iter_with_full_binders sigma g f n c = match kind sigma c with +let iter_with_full_binders sigma g f n c = + let open Context.Rel.Declaration in + match kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () | Cast (c,_,t) -> f n c; f n t - | Prod (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c - | Lambda (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c - | LetIn (na,b,t,c) -> f n b; f n t; f (g (local_def (na, b, t)) n) c + | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c + | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c + | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c | App (c,l) -> f n c; CArray.Fun1.iter f n l | Evar (_,l) -> CArray.Fun1.iter f n l | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> Array.iter (f n) tl; - let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in + let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in Array.iter (f n') bl | CoFix (_,(lna,tl,bl)) -> Array.iter (f n) tl; - let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in + let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in Array.iter (f n') bl let iter_with_binders sigma g f n c = @@ -611,14 +614,14 @@ let rec isArity sigma c = let mkProd_or_LetIn decl c = let open Context.Rel.Declaration in match decl with - | LocalAssum (na,t) -> mkProd (na, of_constr t, c) - | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c) + | LocalAssum (na,t) -> mkProd (na, t, c) + | LocalDef (na,b,t) -> mkLetIn (na, b, t, c) let mkLambda_or_LetIn decl c = let open Context.Rel.Declaration in match decl with - | LocalAssum (na,t) -> mkLambda (na, of_constr t, c) - | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c) + | LocalAssum (na,t) -> mkLambda (na, t, c) + | LocalDef (na,b,t) -> mkLetIn (na, b, t, c) let mkNamedProd id typ c = mkProd (Name id, typ, Vars.subst_var id c) let mkNamedLambda id typ c = mkLambda (Name id, typ, Vars.subst_var id c) @@ -627,18 +630,56 @@ let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, Vars.subst_var id c2) let mkNamedProd_or_LetIn decl c = let open Context.Named.Declaration in match decl with - | LocalAssum (id,t) -> mkNamedProd id (of_constr t) c - | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c + | LocalAssum (id,t) -> mkNamedProd id t c + | LocalDef (id,b,t) -> mkNamedLetIn id b t c let mkNamedLambda_or_LetIn decl c = let open Context.Named.Declaration in match decl with - | LocalAssum (id,t) -> mkNamedLambda id (of_constr t) c - | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c + | LocalAssum (id,t) -> mkNamedLambda id t c + | LocalDef (id,b,t) -> mkNamedLetIn id b t c let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx +open Context +open Environ + +let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl + +let cast_rel_decl : + type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt = + fun Refl x -> x + +let cast_rel_context : + type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt = + fun Refl x -> x + +let cast_named_decl : + type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt = + fun Refl x -> x + +let cast_named_context : + type a b. (a,b) eq -> (a, a) Named.pt -> (b, b) Named.pt = + fun Refl x -> x + +let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e +let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e +let push_named d e = push_named (cast_named_decl unsafe_eq d) e +let push_named_context d e = push_named_context (cast_named_context unsafe_eq d) e +let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq d) e + +let rel_context e = cast_rel_context (sym unsafe_eq) (rel_context e) +let named_context e = cast_named_context (sym unsafe_eq) (named_context e) + +let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq e) +let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e) + +let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e) +let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e) +let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e) + + module Unsafe = struct let to_constr = unsafe_to_constr diff --git a/engine/eConstr.mli b/engine/eConstr.mli index cb671154c..d6b2113d2 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -10,6 +10,7 @@ open CSig open Names open Constr open Context +open Environ type t (** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring @@ -22,6 +23,10 @@ type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint type unsafe_judgment = (constr, types) Environ.punsafe_judgment type unsafe_type_judgment = types Environ.punsafe_type_judgment +type named_declaration = (constr, types) Context.Named.Declaration.pt +type rel_declaration = (constr, types) Context.Rel.Declaration.pt +type named_context = (constr, types) Context.Named.pt +type rel_context = (constr, types) Context.Rel.pt (** {5 Destructors} *) @@ -77,16 +82,16 @@ val mkArrow : t -> t -> t val applist : t * t list -> t -val mkProd_or_LetIn : Rel.Declaration.t -> t -> t -val mkLambda_or_LetIn : Rel.Declaration.t -> t -> t -val it_mkProd_or_LetIn : t -> Rel.t -> t -val it_mkLambda_or_LetIn : t -> Rel.t -> t +val mkProd_or_LetIn : rel_declaration -> t -> t +val mkLambda_or_LetIn : rel_declaration -> t -> t +val it_mkProd_or_LetIn : t -> rel_context -> t +val it_mkLambda_or_LetIn : t -> rel_context -> t val mkNamedLambda : Id.t -> types -> constr -> constr val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr val mkNamedProd : Id.t -> types -> types -> types -val mkNamedLambda_or_LetIn : Named.Declaration.t -> types -> types -val mkNamedProd_or_LetIn : Named.Declaration.t -> types -> types +val mkNamedLambda_or_LetIn : named_declaration -> types -> types +val mkNamedProd_or_LetIn : named_declaration -> types -> types (** {6 Simple case analysis} *) @@ -131,13 +136,13 @@ val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint val decompose_app : Evd.evar_map -> t -> t * t list val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t -val decompose_lam_assum : Evd.evar_map -> t -> Context.Rel.t * t -val decompose_lam_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t -val decompose_lam_n_decls : Evd.evar_map -> int -> t -> Context.Rel.t * t +val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t +val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t +val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t -val decompose_prod_assum : Evd.evar_map -> t -> Context.Rel.t * t -val decompose_prod_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t +val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t +val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t val existential_type : Evd.evar_map -> existential -> types @@ -156,7 +161,7 @@ val map : Evd.evar_map -> (t -> t) -> t -> t val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t val iter : Evd.evar_map -> (t -> unit) -> t -> unit val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit -val iter_with_full_binders : Evd.evar_map -> (Rel.Declaration.t -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit +val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** {6 Substitutions} *) @@ -184,6 +189,25 @@ val subst_univs_level_constr : Univ.universe_level_subst -> t -> t end +(** {5 Environment handling} *) + +val push_rel : rel_declaration -> env -> env +val push_rel_context : rel_context -> env -> env + +val push_named : named_declaration -> env -> env +val push_named_context : named_context -> env -> env +val push_named_context_val : named_declaration -> named_context_val -> named_context_val + +val rel_context : env -> rel_context +val named_context : env -> named_context + +val val_of_named_context : named_context -> named_context_val +val named_context_of_val : named_context_val -> named_context + +val lookup_rel : int -> env -> rel_declaration +val lookup_named : variable -> env -> named_declaration +val lookup_named_val : variable -> named_context_val -> named_declaration + (** {5 Unsafe operations} *) module Unsafe : diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 42620c0b5..0582e34be 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -139,12 +139,12 @@ let nf_named_context_evar sigma ctx = Context.Named.map (nf_evar0 sigma) ctx let nf_rel_context_evar sigma ctx = - Context.Rel.map (nf_evar0 sigma) ctx + Context.Rel.map (nf_evar sigma) ctx let nf_env_evar sigma env = let nc' = nf_named_context_evar sigma (Environ.named_context env) in - let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in - push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) + let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in + EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info @@ -320,7 +320,7 @@ let empty_csubst = (0, Int.Map.empty) type ext_named_context = csubst * (Id.t * EConstr.constr) list * - Id.Set.t * Context.Named.t + Id.Set.t * EConstr.named_context let push_var id (n, s) = let s = Int.Map.add n (EConstr.mkVar id) s in @@ -330,7 +330,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = let open EConstr in let open Vars in let map_decl f d = - NamedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (f (EConstr.of_constr c))) d + NamedDecl.map_constr f d in let replace_var_named_declaration id0 id decl = let id' = NamedDecl.get_id decl in @@ -354,7 +354,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = else (** id_of_name_using_hdchar only depends on the rel context which is empty here *) - next_ident_away (id_of_name_using_hdchar empty_env (RelDecl.get_type decl) na) avoid + next_ident_away (id_of_name_using_hdchar empty_env (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) na) avoid in match extract_if_neq id na with | Some id0 when not (is_section_variable id0) -> @@ -542,6 +542,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = removed *) let evi = Evd.find_undefined !evdref evk in let ctxt = Evd.evar_filtered_context evi in + let ctxt = List.map (fun d -> map_named_decl EConstr.of_constr d) ctxt in let (rids,filter) = List.fold_right2 (fun h a (ri,filter) -> @@ -595,6 +596,7 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occurring in evi *) + let terms = List.map EConstr.Unsafe.to_constr terms in let global = Id.Set.exists is_section_variable ids in let terms = List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in @@ -616,10 +618,9 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = in remove_hyps ids check_context check_value hyps in - (nhyps,terms) + (nhyps,List.map EConstr.of_constr terms) let clear_hyps_in_evi env evdref hyps concl ids = - let concl = EConstr.Unsafe.to_constr concl in match clear_hyps_in_evi_main env evdref hyps [concl] ids with | (nhyps,[nconcl]) -> (nhyps,nconcl) | _ -> assert false @@ -746,6 +747,7 @@ let occur_evar_upto sigma n c = any type has type Type. May cause some trouble, but not so far... *) let judge_of_new_Type evd = + let open EConstr in let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 67de18abc..2da4f8043 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -10,6 +10,7 @@ open Names open Term open Evd open Environ +open EConstr (** This module provides useful higher-level functions for evar manipulation. *) @@ -17,51 +18,51 @@ open Environ (** [new_meta] is a generator of unique meta variables *) val new_meta : unit -> metavariable -val mk_new_meta : unit -> EConstr.constr +val mk_new_meta : unit -> 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:EConstr.constr list -> ?store:Store.t -> + ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> EConstr.types -> (EConstr.constr, 'r) Sigma.sigma + ?principal:bool -> types -> (constr, 'r) Sigma.sigma val new_pure_evar : named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:EConstr.constr list -> ?store:Store.t -> + ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> EConstr.types -> (evar, 'r) Sigma.sigma + ?principal:bool -> types -> (evar, 'r) Sigma.sigma 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:EConstr.constr list -> ?store:Store.t -> + ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> EConstr.types -> EConstr.constr + ?principal:bool -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> - (EConstr.constr * sorts, 'r) Sigma.sigma + (constr * sorts, 'r) Sigma.sigma val e_new_type_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> EConstr.constr * sorts + ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts -val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (EConstr.constr, 'r) Sigma.sigma -val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> EConstr.constr +val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma +val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> - EConstr.constr list option -> (existential_key, 'r) Sigma.sigma + constr list option -> (existential_key, 'r) Sigma.sigma (** Polymorphic constants *) -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 +val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma +val e_new_global : evar_map ref -> Globnames.global_reference -> 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 @@ -70,15 +71,15 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> EConstr.constr of [inst] are typed in the occurrence context and their type (seen 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:EConstr.constr list -> + named_context_val -> 'r Sigma.t -> types -> + ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> - EConstr.constr list -> (EConstr.constr, 'r) Sigma.sigma + constr list -> (constr, 'r) Sigma.sigma val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list -val safe_evar_value : evar_map -> existential -> constr option +val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option (** {6 Evars/Metas switching...} *) @@ -88,15 +89,15 @@ val non_instantiated : evar_map -> evar_info Evar.Map.t (** [head_evar c] returns the head evar of [c] if any *) exception NoHeadEvar -val head_evar : evar_map -> EConstr.constr -> existential_key (** may raise NoHeadEvar *) +val head_evar : evar_map -> constr -> existential_key (** may raise NoHeadEvar *) (* Expand head evar if any *) -val whd_head_evar : evar_map -> EConstr.constr -> EConstr.constr +val whd_head_evar : evar_map -> constr -> constr (* An over-approximation of [has_undefined (nf_evars evd c)] *) -val has_undefined_evars : evar_map -> EConstr.constr -> bool +val has_undefined_evars : evar_map -> constr -> bool -val is_ground_term : evar_map -> EConstr.constr -> bool +val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool (** [gather_dependent_evars evm seeds] classifies the evars in [evm] @@ -121,14 +122,14 @@ val advance : evar_map -> evar -> evar option This is roughly a combination of the previous functions and [nf_evar]. *) -val undefined_evars_of_term : evar_map -> EConstr.constr -> Evar.Set.t +val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t (** [occur_evar_upto sigma k c] returns [true] if [k] appears in [c]. It looks up recursively in [sigma] for the value of existential variables. *) -val occur_evar_upto : evar_map -> Evar.t -> EConstr.t -> bool +val occur_evar_upto : evar_map -> Evar.t -> constr -> bool (** {6 Value/Type constraints} *) @@ -139,18 +140,18 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains uninstantiated; [nf_evar] leaves uninstantiated evars as is *) -val whd_evar : evar_map -> EConstr.constr -> EConstr.constr -val nf_evar : evar_map -> EConstr.constr -> EConstr.constr -val j_nf_evar : evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment +val whd_evar : evar_map -> constr -> constr +val nf_evar : evar_map -> constr -> constr +val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment val jl_nf_evar : - evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list + evar_map -> unsafe_judgment list -> unsafe_judgment list val jv_nf_evar : - evar_map -> EConstr.unsafe_judgment array -> EConstr.unsafe_judgment array + evar_map -> unsafe_judgment array -> unsafe_judgment array val tj_nf_evar : - evar_map -> EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment + evar_map -> unsafe_type_judgment -> unsafe_type_judgment val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t -val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t +val nf_rel_context_evar : evar_map -> rel_context -> rel_context val nf_env_evar : evar_map -> env -> env val nf_evar_info : evar_map -> evar_info -> evar_info @@ -159,39 +160,39 @@ val nf_evar_map_undefined : evar_map -> evar_map (** Presenting terms without solved evars *) -val nf_evars_universes : evar_map -> constr -> constr +val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr -val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr) -val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst +val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst (** Normalize the evar map w.r.t. universes, after simplification of constraints. Return the substitution function for constrs as well. *) -val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr) +val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of existential_key -val flush_and_check_evars : evar_map -> EConstr.constr -> constr +val flush_and_check_evars : evar_map -> constr -> Constr.constr (** {6 Term manipulation up to instantiation} *) (** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t] as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the value of [e] in [sigma] is (recursively) used. *) -val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term +val kind_of_term_upto : evar_map -> Constr.constr -> (Constr.constr,Constr.types) kind_of_term (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are assumed to be an extention of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool +val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool (** {6 Removing hyps in evars'context} raise OccurHypInSimpleClause if the removal breaks dependencies *) type clear_dependency_error = | OccurHypInSimpleClause of Id.t option -| EvarTypingBreak of existential +| EvarTypingBreak of Constr.existential exception ClearDependencyError of Id.t * clear_dependency_error @@ -199,7 +200,7 @@ exception ClearDependencyError of Id.t * clear_dependency_error used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*) val cleared : bool Store.field -val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> EConstr.types -> +val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> Id.Set.t -> named_context_val * types val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> @@ -208,19 +209,19 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty type csubst val empty_csubst : csubst -val csubst_subst : csubst -> EConstr.t -> EConstr.t +val csubst_subst : csubst -> constr -> constr type ext_named_context = - csubst * (Id.t * EConstr.constr) list * - Id.Set.t * Context.Named.t + csubst * (Id.t * constr) list * + Id.Set.t * named_context val push_rel_decl_to_named_context : - Context.Rel.Declaration.t -> ext_named_context -> ext_named_context + rel_declaration -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : Environ.env -> EConstr.types -> - named_context_val * EConstr.types * EConstr.constr list * csubst * (identifier*EConstr.constr) list +val push_rel_context_to_named_context : Environ.env -> types -> + named_context_val * types * constr list * csubst * (identifier*constr) list -val generalize_evar_over_rels : evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list +val generalize_evar_over_rels : evar_map -> existential -> types * constr list (** Evar combinators *) @@ -235,5 +236,5 @@ val meta_counter_summary_name : string (** Deprecater *) -type type_constraint = EConstr.types option -type val_constraint = EConstr.constr option +type type_constraint = types option +type val_constraint = constr option diff --git a/engine/proofview.ml b/engine/proofview.ml index ab72cc405..0a18cf191 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -995,7 +995,7 @@ module Goal = struct let env { env=env } = env let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma - let hyps { env=env } = Environ.named_context env + let hyps { env=env } = EConstr.named_context env let concl { concl=concl } = concl let extra { sigma=sigma; self=self } = goal_extra sigma self diff --git a/engine/proofview.mli b/engine/proofview.mli index 9f10e874a..025e3de20 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -14,6 +14,7 @@ open Util open Term +open EConstr (** Main state of tactics *) type proofview @@ -43,7 +44,7 @@ val compact : entry -> proofview -> entry * proofview empty [evar_map] (indeed a proof can be triggered by an incomplete pretyping), [init] takes an additional argument to represent the initial [evar_map]. *) -val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofview +val init : Evd.evar_map -> (Environ.env * types) list -> entry * proofview (** A [telescope] is a list of environment and conclusion like in {!init}, except that each element may depend on the previous @@ -52,7 +53,7 @@ val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofvi [evar_map] is threaded in state passing style. *) type telescope = | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) + | TCons of Environ.env * Evd.evar_map * types * (Evd.evar_map -> constr -> telescope) (** Like {!init}, but goals are allowed to be dependent on one another. Dependencies between goals is represented with the type @@ -69,8 +70,8 @@ val finished : proofview -> bool (** Returns the current [evar] state. *) val return : proofview -> Evd.evar_map -val partial_proof : entry -> proofview -> EConstr.constr list -val initial_goals : entry -> (EConstr.constr * EConstr.types) list +val partial_proof : entry -> proofview -> constr list +val initial_goals : entry -> (constr * types) list @@ -484,15 +485,15 @@ module Goal : sig respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : ([ `NF ], 'r) t -> EConstr.constr - val hyps : ([ `NF ], 'r) t -> Context.Named.t + val concl : ([ `NF ], 'r) t -> constr + val hyps : ([ `NF ], 'r) t -> named_context val env : ('a, 'r) t -> Environ.env val sigma : ('a, 'r) t -> 'r Sigma.t val extra : ('a, 'r) t -> Evd.Store.t (** Returns the goal's conclusion even if the goal is not normalised. *) - val raw_concl : ('a, 'r) t -> EConstr.constr + val raw_concl : ('a, 'r) t -> constr type ('a, 'b) enter = { enter : 'r. ('a, 'r) t -> 'b } diff --git a/engine/termops.ml b/engine/termops.ml index 46e9ad927..c35e92f97 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -167,19 +167,10 @@ let rel_list n m = in reln [] 1 -let local_assum (na, t) = - let open RelDecl in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let open RelDecl in - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - let push_rel_assum (x,t) env = let open RelDecl in - push_rel (local_assum (x,t)) env + let open EConstr in + push_rel (LocalAssum (x,t)) env let push_rels_assum assums = let open RelDecl in @@ -218,8 +209,8 @@ let mkProd_wo_LetIn decl c = let open EConstr in let open RelDecl in match decl with - | LocalAssum (na,t) -> mkProd (na, EConstr.of_constr t, c) - | LocalDef (_,b,_) -> Vars.subst1 (EConstr.of_constr b) c + | LocalAssum (na,t) -> mkProd (na, t, c) + | LocalDef (_,b,_) -> Vars.subst1 b c let it_mkProd init = List.fold_left (fun c (n,t) -> EConstr.mkProd (n, t, c)) init let it_mkLambda init = List.fold_left (fun c (n,t) -> EConstr.mkLambda (n, t, c)) init @@ -334,7 +325,8 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with let fold_rec_types g (lna,typarray,_) e = let open EConstr in - let ctxt = Array.map2_i (fun i na t -> local_assum (na, Vars.lift i t)) lna typarray in + let open Vars in + let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> g assum e) e ctxt let map_left2 f a g b = @@ -350,6 +342,7 @@ let map_left2 f a g b = end let map_constr_with_binders_left_to_right sigma g f l c = + let open RelDecl in let open EConstr in match EConstr.kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ @@ -361,18 +354,18 @@ let map_constr_with_binders_left_to_right sigma g f l c = else mkCast (b',k,t') | Prod (na,t,b) -> let t' = f l t in - let b' = f (g (local_assum (na,t)) l) b in + let b' = f (g (LocalAssum (na,t)) l) b in if t' == t && b' == b then c else mkProd (na, t', b') | Lambda (na,t,b) -> let t' = f l t in - let b' = f (g (local_assum (na,t)) l) b in + let b' = f (g (LocalAssum (na,t)) l) b in if t' == t && b' == b then c else mkLambda (na, t', b') | LetIn (na,bo,t,b) -> let bo' = f l bo in let t' = f l t in - let b' = f (g (local_def (na,bo,t)) l) b in + let b' = f (g (LocalDef (na,bo,t)) l) b in if bo' == bo && t' == t && b' == b then c else mkLetIn (na, bo', t', b') | App (c,[||]) -> assert false @@ -414,7 +407,6 @@ let map_constr_with_binders_left_to_right sigma g f l c = (* strong *) let map_constr_with_full_binders sigma g f l cstr = - let inj c = EConstr.Unsafe.to_constr c in let open EConstr in let open RelDecl in match EConstr.kind sigma cstr with @@ -426,16 +418,16 @@ let map_constr_with_full_binders sigma g f l cstr = if c==c' && t==t' then cstr else mkCast (c', k, t') | Prod (na,t,c) -> let t' = f l t in - let c' = f (g (LocalAssum (na, inj t)) l) c in + let c' = f (g (LocalAssum (na, t)) l) c in if t==t' && c==c' then cstr else mkProd (na, t', c') | Lambda (na,t,c) -> let t' = f l t in - let c' = f (g (LocalAssum (na, inj t)) l) c in + let c' = f (g (LocalAssum (na, t)) l) c in if t==t' && c==c' then cstr else mkLambda (na, t', c') | LetIn (na,b,t,c) -> let b' = f l b in let t' = f l t in - let c' = f (g (LocalDef (na, inj b, inj t)) l) c in + let c' = f (g (LocalDef (na, b, t)) l) c in if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c') | App (c,al) -> let c' = f l c in @@ -456,7 +448,7 @@ let map_constr_with_full_binders sigma g f l cstr = | Fix (ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in + Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -464,7 +456,7 @@ let map_constr_with_full_binders sigma g f l cstr = | CoFix(ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in + Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -577,10 +569,10 @@ let occur_var env sigma id c = let occur_var_in_decl env sigma hyp decl = let open NamedDecl in match decl with - | LocalAssum (_,typ) -> occur_var env sigma hyp (EConstr.of_constr typ) + | LocalAssum (_,typ) -> occur_var env sigma hyp typ | LocalDef (_, body, typ) -> - occur_var env sigma hyp (EConstr.of_constr typ) || - occur_var env sigma hyp (EConstr.of_constr body) + occur_var env sigma hyp typ || + occur_var env sigma hyp body let local_occur_var sigma id c = let rec occur c = match EConstr.kind sigma c with @@ -655,8 +647,8 @@ let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t let dependent_in_decl sigma a decl = let open NamedDecl in match decl with - | LocalAssum (_,t) -> dependent sigma a (EConstr.of_constr t) - | LocalDef (_, body, t) -> dependent sigma a (EConstr.of_constr body) || dependent sigma a (EConstr.of_constr t) + | LocalAssum (_,t) -> dependent sigma a t + | LocalDef (_, body, t) -> dependent sigma a body || dependent sigma a t let count_occurrences sigma m t = let open EConstr in @@ -886,7 +878,7 @@ let eq_constr sigma t1 t2 = constr_cmp sigma Reduction.CONV t1 t2 (* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn) App(c,[||]) -> ([],c) *) -let split_app c = match kind_of_term c with +let split_app sigma c = match EConstr.kind sigma c with App(c,l) -> let len = Array.length l in if Int.equal len 0 then ([],c) else @@ -895,28 +887,30 @@ let split_app c = match kind_of_term c with c::(Array.to_list prev), last | _ -> assert false -type subst = (Context.Rel.t * constr) Evar.Map.t +type subst = (EConstr.rel_context * EConstr.constr) Evar.Map.t exception CannotFilter let filtering sigma env cv_pb c1 c2 = + let open EConstr in + let open Vars in let evm = ref Evar.Map.empty in let define cv_pb e1 ev c1 = try let (e2,c2) = Evar.Map.find ev !evm in let shift = List.length e1 - List.length e2 in - if constr_cmp sigma cv_pb (EConstr.of_constr c1) (EConstr.of_constr (lift shift c2)) then () else raise CannotFilter + if constr_cmp sigma cv_pb c1 (lift shift c2) then () else raise CannotFilter with Not_found -> evm := Evar.Map.add ev (e1,c1) !evm in let rec aux env cv_pb c1 c2 = - match kind_of_term c1, kind_of_term c2 with + match EConstr.kind sigma c1, EConstr.kind sigma c2 with | App _, App _ -> - let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in + let ((p1,l1),(p2,l2)) = (split_app sigma c1),(split_app sigma c2) in let () = aux env cv_pb l1 l2 in begin match p1, p2 with | [], [] -> () | (h1 :: p1), (h2 :: p2) -> - aux env cv_pb (applistc h1 p1) (applistc h2 p2) + aux env cv_pb (applist (h1, p1)) (applist (h2, p2)) | _ -> assert false end | Prod (n,t1,c1), Prod (_,t2,c2) -> @@ -925,21 +919,20 @@ let filtering sigma env cv_pb c1 c2 = | _, Evar (ev,_) -> define cv_pb env ev c1 | Evar (ev,_), _ -> define cv_pb env ev c2 | _ -> - let inj = EConstr.Unsafe.to_constr in if compare_constr_univ sigma - (fun pb c1 c2 -> aux env pb (inj c1) (inj c2); true) cv_pb (EConstr.of_constr c1) (EConstr.of_constr c2) then () + (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then () else raise CannotFilter (* TODO: le reste des binders *) in aux env cv_pb c1 c2; !evm let decompose_prod_letin sigma c = - let rec prodec_rec i l sigma c = match EConstr.kind sigma c with - | 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, c in - prodec_rec 0 [] sigma c + let rec prodec_rec i l c = match EConstr.kind sigma c with + | Prod (n,t,c) -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c + | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c + | Cast (c,_,_) -> prodec_rec i l c + | _ -> i,l,c in + prodec_rec 0 [] c (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction * gives n (casts are ignored) *) @@ -1007,7 +1000,7 @@ let rec eta_reduce_head sigma c = (* iterator on rel context *) let process_rel_context f env = let sign = named_context_val env in - let rels = rel_context env in + let rels = EConstr.rel_context env in let env0 = reset_with_named_context sign env in Context.Rel.fold_outside f rels ~init:env0 @@ -1055,6 +1048,14 @@ let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let mem_named_context_val id ctxt = try Environ.lookup_named_val id ctxt; true with Not_found -> false +let map_rel_decl f = function +| RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t) +| RelDecl.LocalDef (id, b, t) -> RelDecl.LocalDef (id, f b, f t) + +let map_named_decl f = function +| NamedDecl.LocalAssum (id, t) -> NamedDecl.LocalAssum (id, f t) +| NamedDecl.LocalDef (id, b, t) -> NamedDecl.LocalDef (id, f b, f t) + let compact_named_context sign = let compact l decl = match decl, l with @@ -1098,10 +1099,10 @@ let global_vars_set env sigma constr = let global_vars env sigma ids = Id.Set.elements (global_vars_set env sigma ids) let global_vars_set_of_decl env sigma = function - | NamedDecl.LocalAssum (_,t) -> global_vars_set env sigma (EConstr.of_constr t) + | NamedDecl.LocalAssum (_,t) -> global_vars_set env sigma t | NamedDecl.LocalDef (_,c,t) -> - Id.Set.union (global_vars_set env sigma (EConstr.of_constr t)) - (global_vars_set env sigma (EConstr.of_constr c)) + Id.Set.union (global_vars_set env sigma t) + (global_vars_set env sigma c) let dependency_closure env sigma sign hyps = if Id.Set.is_empty hyps then [] else @@ -1155,6 +1156,7 @@ let context_chop k ctx = (* Do not skip let-in's *) let env_rel_context_chop k env = + let open EConstr in let rels = rel_context env in let ctx1,ctx2 = List.chop k rels in push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), diff --git a/engine/termops.mli b/engine/termops.mli index 196962354..841de34b1 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -34,7 +34,7 @@ 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.constr option * Constr.types +val lookup_rel_id : Id.t -> ('c, 't) Context.Rel.pt -> int * 'c option * 't (** Associates the contents of an identifier in a [rel_context]. Raise [Not_found] if there is no such identifier. *) @@ -45,16 +45,16 @@ 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 -> types -> types +val mkProd_or_LetIn : rel_declaration -> types -> types +val mkProd_wo_LetIn : rel_declaration -> 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 : types -> Context.Rel.t -> types +val it_mkProd_or_LetIn : types -> rel_context -> types +val it_mkProd_wo_LetIn : types -> rel_context -> 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_or_LetIn : types -> named_context -> types val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types -val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr +val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) @@ -64,12 +64,12 @@ val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Const val map_constr_with_binders_left_to_right : Evd.evar_map -> - (Context.Rel.Declaration.t -> 'a -> 'a) -> + (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_full_binders : Evd.evar_map -> - (Context.Rel.Declaration.t -> 'a -> 'a) -> + (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate @@ -105,7 +105,7 @@ 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 + Id.t -> named_declaration -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool @@ -117,7 +117,7 @@ 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 dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> 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 *) @@ -182,11 +182,11 @@ 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.constr) Evar.Map.t -val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> Constr.constr -> Constr.constr -> subst +type subst = (rel_context * constr) Evar.Map.t +val filtering : Evd.evar_map -> rel_context -> Reduction.conv_pb -> constr -> constr -> subst -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 +val decompose_prod_letin : Evd.evar_map -> constr -> int * rel_context * constr +val align_prod_letin : Evd.evar_map -> constr -> constr -> rel_context * constr (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction gives {% $ %}n{% $ %} (casts are ignored) *) @@ -215,8 +215,8 @@ val add_name : Name.t -> names_context -> names_context val lookup_name_of_rel : int -> names_context -> Name.t val lookup_rel_of_name : Id.t -> names_context -> int val empty_names_context : names_context -val ids_of_rel_context : Context.Rel.t -> Id.t list -val ids_of_named_context : Context.Named.t -> Id.t list +val ids_of_rel_context : ('c, 't) Context.Rel.pt -> Id.t list +val ids_of_named_context : ('c, 't) Context.Named.pt -> Id.t list val ids_of_context : env -> Id.t list val names_of_rel_context : env -> names_context @@ -228,15 +228,15 @@ val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t (* [env_rel_context_chop n env] extracts out the [n] top declarations of the rel_context part of [env], counting both local definitions and hypotheses *) -val env_rel_context_chop : int -> env -> env * Context.Rel.t +val env_rel_context_chop : int -> env -> env * rel_context (** Set of local names *) val vars_of_env: env -> Id.Set.t 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.constr) list +val process_rel_context : (rel_declaration -> env -> env) -> env -> env +val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list val lift_rel_context : int -> 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 *) @@ -244,23 +244,26 @@ val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in contex val map_rel_context_in_env : (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t val map_rel_context_with_binders : - (int -> Constr.constr -> Constr.constr) -> Context.Rel.t -> Context.Rel.t + (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt val fold_named_context_both_sides : ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> Context.Named.t -> init:'a -> 'a val mem_named_context_val : Id.t -> named_context_val -> bool val compact_named_context : Context.Named.t -> Context.Compacted.t +val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt +val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt + val clear_named_body : Id.t -> env -> env 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_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t 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 *) -val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> Id.t list +val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.t list (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e5dd6a6ec..41e2e4e6f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2083,6 +2083,7 @@ let intern_context global_level env impl_env binders = user_err ~loc ~hdr:"internalize" (explain_internalization_error e) let interp_rawcontext_evars env evdref k bl = + let open EConstr in let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> @@ -2093,7 +2094,6 @@ let interp_rawcontext_evars env evdref k bl = let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> - let t = EConstr.Unsafe.to_constr t in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2104,8 +2104,6 @@ let interp_rawcontext_evars env evdref k bl = (push_rel d env, d::params, succ n, impls) | Some b -> let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in - let t = EConstr.Unsafe.to_constr t in - let c = EConstr.Unsafe.to_constr c in let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 2f6795ed4..ae7f511f4 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -160,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map ref -> local_binder list -> - internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits) + internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) @@ -177,7 +177,7 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : Context.Named.t -> Id.t -> constr +val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr val global_reference : Id.t -> constr val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index c942e8e92..b45ead217 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -41,22 +41,6 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration module RelDecl = Context.Rel.Declaration -let local_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - RelDecl.LocalAssum (na, inj t) - -let local_def (na, b, t) = - let inj = EConstr.Unsafe.to_constr in - RelDecl.LocalDef (na, inj b, inj t) - -let nlocal_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - NamedDecl.LocalAssum (na, inj t) - -let nlocal_def (na, b, t) = - let inj = EConstr.Unsafe.to_constr in - NamedDecl.LocalDef (na, inj b, inj t) - (** Typeclass-based generalized rewriting. *) (** Constants used by the tactic. *) @@ -251,7 +235,7 @@ end) = struct evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs else let (evars, b, arg, cstrs) = - aux (Environ.push_rel (local_assum (na, ty)) env) evars b cstrs + aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs in let ty = Reductionops.nf_betaiota (goalevars evars) ty in let pred = mkLambda (na, ty, b) in @@ -350,7 +334,7 @@ end) = struct let evars, rb = aux evars env b' (pred n) in app_poly env evars pointwise_relation [| ty; b'; rb |] else - let evars, rb = aux evars (Environ.push_rel (local_assum (na, ty)) env) b (pred n) in + let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in app_poly env evars forall_relation [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |] | _ -> raise Not_found @@ -379,7 +363,7 @@ end) = struct else (try let params, args = Array.chop (Array.length args - 2) args in - let env' = Environ.push_rel_context rels env in + let env' = push_rel_context rels env in let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in let evars = Sigma.to_evar_map evars in @@ -546,7 +530,7 @@ let decompose_applied_relation env sigma (c,l) = | Some c -> c | None -> let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *) - match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> local_assum (n, t)) ctx)) with + match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with | Some c -> c | None -> error "Cannot find an homogeneous relation to rewrite." @@ -826,8 +810,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev if b then PropGlobal.do_subrelation, PropGlobal.apply_subrelation else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation in - Environ.push_named - (nlocal_def (Id.of_string "do_subrelation", + EConstr.push_named + (LocalDef (Id.of_string "do_subrelation", snd (app_poly_sort b env evars dosub [||]), snd (app_poly_nocheck env evars appsub [||]))) env @@ -947,7 +931,7 @@ let fold_match ?(force=false) env sigma c = let dep, pred, exists, (sk,eff) = let env', ctx, body = let ctx, pred = decompose_lam_assum sigma p in - let env' = Environ.push_rel_context ctx env in + let env' = push_rel_context ctx env in env', ctx, pred in let sortp = Retyping.get_sort_family_of env' sigma body in @@ -1174,7 +1158,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Lambda (n, t, b) when flags.under_lambdas -> let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in let open Context.Rel.Declaration in - let env' = Environ.push_rel (local_assum (n', t)) env in + let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in let state, b' = s.strategy { state ; env = env' ; unfresh ; @@ -1563,15 +1547,14 @@ let assert_replacing id newt tac = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let ctx = Environ.named_context env in + let ctx = named_context env in let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in let nc = match before with | [] -> assert false - | d :: rem -> insert_dependent env sigma (nlocal_assum (NamedDecl.get_id d, newt)) [] after @ rem + | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Refine.refine ~unsafe:false { run = begin fun sigma -> - let open EConstr in let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in let map d = @@ -1612,7 +1595,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id) | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_hyp_no_check (nlocal_assum (id, newt)) <*> + convert_hyp_no_check (LocalAssum (id, newt)) <*> beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> @@ -1640,10 +1623,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = | None -> env | Some id -> (** Only consider variables not depending on [id] *) - let ctx = Environ.named_context env in + let ctx = named_context env in let filter decl = not (occur_var_in_decl env sigma id decl) in let nctx = List.filter filter ctx in - Environ.reset_with_named_context (Environ.val_of_named_context nctx) env + Environ.reset_with_named_context (val_of_named_context nctx) env in try let res = diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli index 378359d51..10fec2032 100644 --- a/ltac/rewrite.mli +++ b/ltac/rewrite.mli @@ -8,8 +8,8 @@ open Names open Constr -open EConstr open Environ +open EConstr open Constrexpr open Tacexpr open Misctypes @@ -75,7 +75,7 @@ val cl_rewrite_clause : bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic val is_applied_rewrite_relation : - env -> evar_map -> Context.Rel.t -> constr -> types option + env -> evar_map -> rel_context -> constr -> types option val declare_relation : ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t -> diff --git a/ltac/tactic_matching.ml b/ltac/tactic_matching.ml index ac64f0bba..5b5cd06cc 100644 --- a/ltac/tactic_matching.ml +++ b/ltac/tactic_matching.ml @@ -284,7 +284,7 @@ module PatternMatching (E:StaticEnvironment) = struct pick hyps >>= fun decl -> let id = NamedDecl.get_id decl in let refresh = is_local_def decl in - pattern_match_term refresh pat (EConstr.of_constr (NamedDecl.get_type decl)) () <*> + pattern_match_term refresh pat (NamedDecl.get_type decl) () <*> put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*> return id @@ -295,8 +295,6 @@ module PatternMatching (E:StaticEnvironment) = struct let hyp_match_body_and_type hypname bodypat typepat hyps = pick hyps >>= function | LocalDef (id,body,hyp) -> - let body = EConstr.of_constr body in - let hyp = EConstr.of_constr hyp in pattern_match_term false bodypat body () <*> pattern_match_term true typepat hyp () <*> put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*> diff --git a/ltac/tactic_matching.mli b/ltac/tactic_matching.mli index d6f67d6c7..300b546f1 100644 --- a/ltac/tactic_matching.mli +++ b/ltac/tactic_matching.mli @@ -43,7 +43,7 @@ val match_term : val match_goal: Environ.env -> Evd.evar_map -> - Context.Named.t -> + EConstr.named_context -> EConstr.constr -> (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 53c450116..5d894c677 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -28,10 +28,6 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let local_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - RelDecl.LocalAssum (na, inj t) - let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) let _f_equal = reference ["Init";"Logic"] "f_equal" @@ -160,7 +156,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr (Environ.push_rel (local_assum (id,atom)) env) sigma (succ nrels) ff + quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts @@ -175,7 +171,7 @@ let litteral_of_constr env sigma term= else begin try - quantified_atom_of_constr (Environ.push_rel (local_assum (id,atom)) env) sigma 1 ff + quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index da971fffb..adc4ad8a3 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -49,7 +49,7 @@ let clear ids { it = goal; sigma } = user_err (str "Cannot clear " ++ pr_id id) in let sigma = !evdref in - let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps (EConstr.of_constr concl) (Goal.V82.extra sigma goal) in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in { it = [gl]; sigma } @@ -638,7 +638,7 @@ let assume_tac hyps gls = tclTHEN (push_intro_tac (fun id -> - Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it)))) st.st_label)) hyps tclIDTAC gls let assume_hyps_or_theses hyps gls = @@ -648,7 +648,7 @@ let assume_hyps_or_theses hyps gls = tclTHEN (push_intro_tac (fun id -> - Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,c)))) nam) + Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr c)))) nam) | Hprop {st_label=nam;st_it=Thesis (tk)} -> tclTHEN (push_intro_tac @@ -660,7 +660,7 @@ let assume_st hyps gls = (fun st -> tclTHEN (push_intro_tac - (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label)) + (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it)))) st.st_label)) hyps tclIDTAC gls let assume_st_letin hyps gls = @@ -669,7 +669,7 @@ let assume_st_letin hyps gls = tclTHEN (push_intro_tac (fun id -> - Proofview.V82.of_tactic (convert_hyp (LocalDef (id, fst st.st_it, snd st.st_it)))) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (LocalDef (id, EConstr.of_constr (fst st.st_it), EConstr.of_constr (snd st.st_it))))) st.st_label)) hyps tclIDTAC gls (* suffices *) @@ -763,7 +763,7 @@ let rec consider_match may_intro introduced available expected gls = error "Not enough sub-hypotheses to match statements." (* should tell which ones *) | id::rest_ids,(Hvar st | Hprop st)::rest -> - tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) + tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it)))) begin match st.st_label with Anonymous -> @@ -834,13 +834,13 @@ let define_tac id args body gls = (* tactics for reconsider *) let cast_tac id_or_thesis typ gls = + let typ = EConstr.of_constr typ in match id_or_thesis with | This id -> Proofview.V82.of_tactic (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> - let typ = EConstr.of_constr typ in Proofview.V82.of_tactic (convert_concl typ DEFAULTcast) gls (* per cases *) @@ -1290,6 +1290,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let f_ids typ = let sign = (prod_assum (Term.prod_applist typ params)) in + let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in find_intro_names sign gls in let constr_args_ids = Array.map f_ids gen_arities in let case_term = diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 7b7e746f2..8744eacd3 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -858,7 +858,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = let decomp_lams_eta_n n m env c t = let rels = fst (splay_prod_n env none n (EConstr.of_constr t)) in - let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in + let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,EConstr.Unsafe.to_constr c)) rels in let rels',c = decompose_lam c in let d = n - m in (* we'd better keep rels' as long as possible. *) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index ef8172de4..9dc2a51a6 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -117,10 +117,9 @@ let mk_open_instance id idc gl m t= let nid=(fresh_id avoid var_id gl) in let evmap = Sigma.Unsafe.of_evar_map evmap in let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in - let c = EConstr.Unsafe.to_constr c in let evmap = Sigma.to_evar_map evmap in let decl = LocalAssum (Name nid, c) in - aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in + aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in evmap, decls, revt diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 36bd91ab6..a60fd4d8f 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -42,7 +42,7 @@ let wrap n b continue seq gls= List.exists (occur_var_in_decl env (project gls) id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in + add_formula Hyp (VarRef id) (EConstr.Unsafe.to_constr (NamedDecl.get_type nd)) (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index ec73fccb5..e11cbc279 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -190,6 +190,8 @@ type hineq={hname:constr; (* le nom de l'hypothèse *) exception NoIneq let ineq1_of_constr (h,t) = + let h = EConstr.Unsafe.to_constr h in + let t = EConstr.Unsafe.to_constr t in match (kind_of_term t) with | App (f,args) -> (match kind_of_term f with @@ -504,7 +506,7 @@ let rec fourier () = |_-> raise GoalDone with GoalDone -> (* les hypothèses *) - let hyps = List.map (fun (h,t)-> (mkVar h,t)) + let hyps = List.map (fun (h,t)-> (EConstr.mkVar h,t)) (list_of_sign (Proofview.Goal.hyps gl)) in let lineq =ref [] in List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 91b17b9a4..bc64b079c 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -236,7 +236,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta -let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = +let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let nochange ?t' msg = begin observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t ); @@ -315,7 +315,7 @@ 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!"); - (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, EConstr.of_constr (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) ) @@ -544,7 +544,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (scan_type new_context new_t') with Failure "NoChange" -> (* Last thing todo : push the rel in the context and continue *) - scan_type (local_assum (x,t_x) :: context) t' + scan_type (LocalAssum (x,t_x) :: context) t' end end else @@ -933,6 +933,7 @@ let generalize_non_dep hyp g = let to_revert,_ = let open Context.Named.Declaration in Environ.fold_named_context_reverse (fun (clear,keep) decl -> + let decl = map_named_decl EConstr.of_constr decl in let hyp = get_id decl in if Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d0d44b34b..e845db3bc 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -33,9 +33,9 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let princ_type = EConstr.of_constr princ_type in let princ_type_info = compute_elim_sig Evd.empty princ_type (** FIXME *) in let env = Global.env () in - let env_with_params = Environ.push_rel_context princ_type_info.params env in + let env_with_params = EConstr.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in - let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t = + let rec change_predicates_names (avoid:Id.t list) (predicates:EConstr.rel_context) : EConstr.rel_context = match predicates with | [] -> [] | decl :: predicates -> @@ -56,7 +56,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) let change_predicate_sort i decl = let new_sort = sorts.(i) in - let args,_ = decompose_prod (RelDecl.get_type decl) in + let args,_ = decompose_prod (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in let real_args = if princ_type_info.indarg_in_concl then List.tl args @@ -87,17 +87,19 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | _ -> false in let pre_princ = + let open EConstr in it_mkProd_or_LetIn (it_mkProd_or_LetIn (Option.fold_right mkProd_or_LetIn princ_type_info.indarg - (EConstr.Unsafe.to_constr princ_type_info.concl) + princ_type_info.concl ) princ_type_info.args ) princ_type_info.branches in + let pre_princ = EConstr.Unsafe.to_constr pre_princ in let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = match kind_of_term c with @@ -240,7 +242,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Context.Named.Declaration.LocalDef (id,t,b) -> LocalDef (Name (Hashtbl.find tbl id), t, b)) new_predicates) ) - princ_type_info.params + (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params) @@ -251,7 +253,7 @@ let change_property_sort evd toSort princ princName = let change_sort_in_predicate decl = LocalAssum (get_name decl, - let args,ty = decompose_prod (get_type decl) in + let args,ty = decompose_prod (EConstr.Unsafe.to_constr (get_type decl)) in let s = destSort ty in Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty); Term.compose_prod args (mkSort toSort) @@ -270,7 +272,7 @@ let change_property_sort evd toSort princ princName = (it_mkLambda_or_LetIn init (List.map change_sort_in_predicate princ_info.predicates) ) - princ_info.params + (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.params) let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1cde4420e..a7489fb7b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -19,7 +19,7 @@ let is_rec_info sigma scheme_info = let test_branche min acc decl = acc || ( let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (EConstr.of_constr (RelDecl.get_type decl)))) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (RelDecl.get_type decl))) in let free_rels_in_br = Termops.free_rels sigma new_branche in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index dcec2cb74..8f1420940 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -26,12 +26,6 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration -let local_assum (na, t) = - RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t) - -let local_def (na, b, t) = - RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t) - (* Some pretty printing function for debugging purpose *) let pr_binding prc = @@ -147,7 +141,7 @@ let generate_type evd g_to_f f graph i = let fun_ctxt,res_type = match ctxt with | [] | [_] -> anomaly (Pp.str "Not a valid context") - | decl :: fun_ctxt -> fun_ctxt, EConstr.of_constr (RelDecl.get_type decl) + | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl in let rec args_from_decl i accu = function | [] -> accu @@ -187,12 +181,12 @@ let generate_type evd g_to_f f graph i = \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \] i*) let pre_ctxt = - local_assum (Name res_id, lift 1 res_type) :: local_def (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt + LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt in (*i and we can return the solution depending on which lemma type we are defining i*) if g_to_f - then local_assum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph - else local_assum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph + then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph + else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph (* @@ -280,7 +274,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun decl -> List.map (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) - (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (EConstr.of_constr (RelDecl.get_type decl)))))) + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches in @@ -477,7 +471,7 @@ let generalize_dependent_of x hyp g = tclMAP (function | LocalAssum (id,t) when not (Id.equal id hyp) && - (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) + (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) | _ -> tclIDTAC ) (pf_hyps g) @@ -695,7 +689,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (fun decl -> List.map (fun id -> id) - (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (EConstr.of_constr (RelDecl.get_type decl)))) + (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (RelDecl.get_type decl))) ) branches in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 2840193a9..691385fad 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -976,7 +976,7 @@ let funify_branches relinfo nfuns branch = | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches) | _ -> false in (* FIXME: *) - LocalDef (Anonymous,mkProp,mkProp) + LocalDef (Anonymous,EConstr.mkProp,EConstr.mkProp) let relprinctype_to_funprinctype relprinctype nfuns = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 56c6ab054..f5ea32878 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -693,7 +693,7 @@ let mkDestructEq : (fun decl -> let open Context.Named.Declaration in let id = get_id decl in - if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) expr (EConstr.of_constr (get_type decl))) + if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) expr (get_type decl)) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in let type_of_expr = pf_unsafe_type_of g expr in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 9e0d591b6..8c2f0f53f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1706,10 +1706,6 @@ let onClearedName2 id tac = Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] end }) -let local_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - let rec is_Prop sigma c = match EConstr.kind sigma c with | Sort (Prop Null) -> true | Cast (c,_,_) -> is_Prop sigma c @@ -1725,24 +1721,24 @@ let destructure_hyps = | decl::lit -> let i = NamedDecl.get_id decl in Proofview.tclEVARMAP >>= fun sigma -> - begin try match destructurate_prop sigma (EConstr.of_constr (NamedDecl.get_type decl)) with + begin try match destructurate_prop sigma (NamedDecl.get_type decl) with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> (Tacticals.New.tclTHENS (elim_id i) - [ onClearedName i (fun i -> (loop (local_assum (i,t1)::lit))); - onClearedName i (fun i -> (loop (local_assum (i,t2)::lit))) ]) + [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit))); + onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop (local_assum (i1,t1) :: local_assum (i2,t2) :: lit))) + loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit))) | Kapp(Iff,[t1;t2]) -> Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop (local_assum (i1,mkArrow t1 t2) :: local_assum (i2,mkArrow t2 t1) :: lit))) + loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit))) | Kimp(t1,t2) -> (* t1 and t2 might be in Type rather than Prop. For t1, the decidability check will ensure being Prop. *) @@ -1753,7 +1749,7 @@ let destructure_hyps = (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> - (loop (local_assum (i,mk_or (mk_not t1) t2) :: lit)))) + (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit)))) ] else loop lit @@ -1764,7 +1760,7 @@ let destructure_hyps = (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> - (loop (local_assum (i,mk_and (mk_not t1) (mk_not t2)) :: lit)))) + (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(And,[t1;t2]) -> let d1 = decidability t1 in @@ -1773,7 +1769,7 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_and, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop (local_assum (i,mk_or (mk_not t1) (mk_not t2)) :: lit)))) + (loop (LocalAssum (i,mk_or (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(Iff,[t1;t2]) -> let d1 = decidability t1 in @@ -1783,7 +1779,7 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_iff, [| t1; t2; d1; d2; mkVar i |])]); (onClearedName i (fun i -> - (loop (local_assum (i, mk_or (mk_and t1 (mk_not t2)) + (loop (LocalAssum (i, mk_or (mk_and t1 (mk_not t2)) (mk_and (mk_not t1) t2)) :: lit)))) ] | Kimp(t1,t2) -> @@ -1795,14 +1791,14 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_imp, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop (local_assum (i,mk_and t1 (mk_not t2)) :: lit)))) + (loop (LocalAssum (i,mk_and t1 (mk_not t2)) :: lit)))) ] | Kapp(Not,[t]) -> let d = decidability t in Tacticals.New.tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); - (onClearedName i (fun i -> (loop (local_assum (i,t) :: lit)))) + (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit)))) ] | Kapp(op,[t1;t2]) -> (try @@ -1835,12 +1831,12 @@ let destructure_hyps = match destructurate_type sigma (pf_nf typ) with | Kapp(Nat,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (EConstr.Unsafe.to_constr (mkApp (Lazy.force coq_neq, [| t1;t2|]))) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) decl)) (loop lit)) | Kapp(Z,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (EConstr.Unsafe.to_constr (mkApp (Lazy.force coq_Zne, [| t1;t2|]))) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) decl)) (loop lit)) | _ -> loop lit diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 475380512..adb11f4f8 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -66,19 +66,18 @@ let l_E_Or = lazy (constant "E_Or") let l_D_Or = lazy (constant "D_Or") -let special_whd gl= - let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) +let special_whd gl c = + Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c -let special_nf gl= - let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in - (fun t -> CClosure.norm_val infos (CClosure.inject t)) +let special_nf gl c = + Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c type atom_env= {mutable next:int; mutable env:(constr*int) list} let make_atom atom_env term= + let term = EConstr.Unsafe.to_constr term in try let (_,i)= List.find (fun (t,_)-> eq_constr term t) atom_env.env @@ -90,13 +89,17 @@ let make_atom atom_env term= Atom i let rec make_form atom_env gls term = + let open EConstr in + let open Vars in let normalize=special_nf gls in let cciterm=special_whd gls term in - match kind_of_term cciterm with + let sigma = Tacmach.project gls in + let inj = EConstr.Unsafe.to_constr in + match EConstr.kind sigma cciterm with Prod(_,a,b) -> - if EConstr.Vars.noccurn (Tacmach.project gls) 1 (EConstr.of_constr b) && + if noccurn sigma 1 b && Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) (EConstr.of_constr a) == InProp + (pf_env gls) sigma a == InProp then let fa=make_form atom_env gls a in let fb=make_form atom_env gls b in @@ -113,7 +116,7 @@ let rec make_form atom_env gls term = | App(hd,argv) when Int.equal (Array.length argv) 2 -> begin try - let ind, _ = destInd hd in + let ind, _ = destInd sigma hd in if Names.eq_ind ind (fst (Lazy.force li_and)) then let fa=make_form atom_env gls argv.(0) in let fb=make_form atom_env gls argv.(1) in @@ -134,9 +137,9 @@ let rec make_hyps atom_env gls lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps atom_env gls (typ::lenv) rest in - if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id (EConstr.of_constr c)) lenv || + if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv || (Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) (EConstr.of_constr typ) != InProp) + (pf_env gls) (Tacmach.project gls) typ != InProp) then hrec else @@ -264,7 +267,6 @@ let rtauto_tac gls= if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in - let gl = EConstr.Unsafe.to_constr gl in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in let formula= diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 9a14ac6c7..092552364 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -12,13 +12,13 @@ type atom_env= mutable env:(Term.constr*int) list} val make_form : atom_env -> - Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form + Proof_type.goal Tacmach.sigma -> EConstr.types -> Proof_search.form val make_hyps : atom_env -> Proof_type.goal Tacmach.sigma -> - Term.types list -> - Context.Named.t -> + EConstr.types list -> + EConstr.named_context -> (Names.Id.t * Proof_search.form) list val rtauto_tac : Proof_type.tactic diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index bf3e2ac1c..d4579c3a1 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -838,7 +838,7 @@ let rec uniquize = function | Context.Rel.Declaration.LocalAssum _ as x -> x | Context.Rel.Declaration.LocalDef (x,_,y) -> Context.Rel.Declaration.LocalAssum(x,y) in - Environ.push_rel ctx_item env, h' + 1 in + EConstr.push_rel ctx_item env, h' + 1 in let self acc c = EConstr.of_constr (subst_loop acc (EConstr.Unsafe.to_constr c)) in let f = EConstr.of_constr f in let f' = map_constr_with_binders_left_to_right sigma inc_h self acc f in @@ -1091,7 +1091,7 @@ let thin id sigma goal = | None -> sigma | Some (hyps, concl) -> let sigma = !evdref in - let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps (EConstr.of_constr concl) (Goal.V82.extra sigma goal) in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in sigma diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3b5662a24..a5a5fe6d2 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -15,12 +15,12 @@ open Names open Nameops open Term open Termops +open Environ open EConstr open Vars open Namegen open Declarations open Inductiveops -open Environ open Reductionops open Type_errors open Glob_term @@ -38,14 +38,6 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let local_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - RelDecl.LocalAssum (na, inj t) - -let local_def (na, b, t) = - let inj = EConstr.Unsafe.to_constr in - RelDecl.LocalDef (na, inj b, inj t) - (* Pattern-matching errors *) type pattern_matching_error = @@ -150,7 +142,7 @@ type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (bool*(Name.t * constr * (constr * types))) | NonDepAlias - | Abstract of int * Context.Rel.Declaration.t + | Abstract of int * rel_declaration type tomatch_stack = tomatch_status list @@ -261,7 +253,7 @@ type 'a pattern_matching_problem = mat : 'a matrix; caseloc : Loc.t; casestyle : case_style; - typing_function: type_constraint -> env -> evar_map ref -> 'a option -> EConstr.unsafe_judgment } + typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } (*--------------------------------------------------------------------------* * A few functions to infer the inductive type from the patterns instead of * @@ -331,14 +323,12 @@ let binding_vars_of_inductive sigma = function let extract_inductive_data env sigma decl = match decl with | LocalAssum (_,t) -> - let t = EConstr.of_constr t in let tmtyp = try try_find_ind env sigma t None with Not_found -> NotInd (None,t) in let tmtypvars = binding_vars_of_inductive sigma tmtyp in (tmtyp,tmtypvars) | LocalDef (_,_,t) -> - let t = EConstr.of_constr t in (NotInd (None, t), []) let unify_tomatch_with_patterns evdref env loc typ pats realnames = @@ -451,7 +441,7 @@ let remove_current_pattern eqn = let push_current_pattern (cur,ty) eqn = match eqn.patterns with | pat::pats -> - let rhs_env = push_rel (local_def (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in + let rhs_env = push_rel (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } @@ -553,8 +543,8 @@ let dependencies_in_pure_rhs nargs eqns = let dependent_decl sigma a = function - | LocalAssum (na,t) -> dependent sigma a (EConstr.of_constr t) - | LocalDef (na,c,t) -> dependent sigma a (EConstr.of_constr t) || dependent sigma a (EConstr.of_constr c) + | LocalAssum (na,t) -> dependent sigma a t + | LocalDef (na,c,t) -> dependent sigma a t || dependent sigma a c let rec dep_in_tomatch sigma n = function | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l @@ -625,7 +615,7 @@ let relocate_index_tomatch sigma n1 n2 = NonDepAlias :: genrec depth rest | Abstract (i,d) :: rest -> let i = relocate_rel n1 n2 depth i in - Abstract (i, RelDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (relocate_index sigma n1 n2 depth (EConstr.of_constr c))) d) + Abstract (i, RelDecl.map_constr (fun c -> relocate_index sigma n1 n2 depth c) d) :: genrec (depth+1) rest in genrec 0 @@ -658,7 +648,7 @@ let replace_tomatch sigma n c = | NonDepAlias :: rest -> NonDepAlias :: replrec depth rest | Abstract (i,d) :: rest -> - Abstract (i, RelDecl.map_constr (fun t -> EConstr.Unsafe.to_constr (replace_term sigma n c depth (EConstr.of_constr t))) d) + Abstract (i, RelDecl.map_constr (fun t -> replace_term sigma n c depth t) d) :: replrec (depth+1) rest in replrec 0 @@ -683,7 +673,7 @@ let rec liftn_tomatch_stack n depth = function NonDepAlias :: liftn_tomatch_stack n depth rest | Abstract (i,d)::rest -> let i = if i<depth then i else i+n in - Abstract (i, RelDecl.map_constr (CVars.liftn n depth) d) + Abstract (i, RelDecl.map_constr (liftn n depth) d) ::(liftn_tomatch_stack n (depth+1) rest) let lift_tomatch_stack n = liftn_tomatch_stack n 1 @@ -737,7 +727,7 @@ let get_names env sign eqns = (fun (l,avoid) d na -> let na = merge_name - (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env t na) avoid)) + (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env (EConstr.Unsafe.to_constr t) na) avoid)) d na in (na::l,(out_name na)::avoid)) @@ -1145,7 +1135,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with | [], _ -> brs,tomatch,pred,[] | n::deps, Abstract (i,d) :: tomatch -> - let d = map_constr (fun c -> EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c))) d in + let d = map_constr (fun c -> nf_evar evd c) d in let is_d = match d with LocalAssum _ -> false | LocalDef _ -> true in if is_d || List.exists (fun c -> dependent_decl evd (lift k c) d) tocheck && Array.exists (is_dependent_branch evd k) brs then @@ -1215,12 +1205,12 @@ let rec generalize_problem names pb = function | [] -> pb, [] | i::l -> let pb',deps = generalize_problem names pb l in - let d = map_constr (CVars.lift i) (Environ.lookup_rel i pb.env) in + let d = map_constr (lift i) (lookup_rel i pb.env) in begin match d with | LocalDef (Anonymous,_,_) -> pb', deps | _ -> (* for better rendering *) - let d = RelDecl.map_type (fun c -> EConstr.Unsafe.to_constr (whd_betaiota !(pb.evdref) (EConstr.of_constr c))) d in + let d = RelDecl.map_type (fun c -> whd_betaiota !(pb.evdref) c) d in let tomatch = lift_tomatch_stack 1 pb'.tomatch in let tomatch = relocate_index_tomatch !(pb.evdref) (i+1) 1 tomatch in { pb' with @@ -1247,6 +1237,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* build the name x1..xn from the names present in the equations *) (* that had matched constructor C *) let cs_args = const_info.cs_args in + let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs_args in let names,aliasname = get_names pb.env cs_args eqns in let typs = List.map2 RelDecl.set_name names cs_args in @@ -1259,7 +1250,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* We adjust the terms to match in the context they will be once the *) (* context [x1:T1,..,xn:Tn] will have been pushed on the current env *) let typs' = - List.map_i (fun i d -> (mkRel i, map_constr (CVars.lift i) d)) 1 typs in + List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in let extenv = push_rel_context typs pb.env in @@ -1415,7 +1406,7 @@ and shift_problem ((current,t),_,na) pb = let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in let pb = { pb with - env = push_rel (local_def (na,current,ty)) pb.env; + env = push_rel (LocalDef (na,current,ty)) pb.env; tomatch = tomatch; pred = lift_predicate 1 pred tomatch; history = pop_history pb.history; @@ -1463,7 +1454,7 @@ and compile_generalization pb i d rest = ([false]). *) and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = let f c t = - let alias = local_def (na,c,t) in + let alias = LocalDef (na,c,t) in let pb = { pb with env = push_rel alias pb.env; @@ -1601,7 +1592,7 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t = let (p, _, _) = lookup_rel_id x (rel_context extenv) in let rec traverse_local_defs p = match lookup_rel p extenv with - | LocalDef (_,c,_) -> assert (isRel sigma (EConstr.of_constr c)); traverse_local_defs (p + destRel sigma (EConstr.of_constr c)) + | LocalDef (_,c,_) -> assert (isRel sigma c); traverse_local_defs (p + destRel sigma c) | LocalAssum _ -> p in let p = traverse_local_defs p in let u = lift (n' - n) u in @@ -1743,6 +1734,7 @@ let build_inversion_problem loc env sigma tms t = let pat,acc = make_patvar t acc in let indf' = lift_inductive_family n indf in let sign = make_arity_signature env true indf' in + let sign = List.map (fun d -> map_rel_decl EConstr.of_constr d) sign in let patl = pat :: List.rev patl in let patl,sign = recover_and_adjust_alias_names patl sign in let p = List.length patl in @@ -1751,7 +1743,7 @@ let build_inversion_problem loc env sigma tms t = List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in - let d = local_assum (alias_of_pat pat,typ) in + let d = LocalAssum (alias_of_pat pat,typ) in let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in let avoid0 = ids_of_context env in @@ -1768,7 +1760,7 @@ let build_inversion_problem loc env sigma tms t = let n = List.length sign in let decls = - List.map_i (fun i d -> (mkRel i, map_constr (CVars.lift i) d)) 1 sign in + List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in let pb_env = push_rel_context sign env in let decls = @@ -1855,8 +1847,8 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = | NotInd (bo,typ) -> (match t with | None -> (match bo with - | None -> [local_assum (na, lift n typ)] - | Some b -> [local_def (na, lift n b, lift n typ)]) + | None -> [LocalAssum (na, lift n typ)] + | Some b -> [LocalDef (na, lift n b, lift n typ)]) | Some (loc,_,_) -> user_err ~loc (str"Unexpected type annotation for a term of non inductive type.")) @@ -1865,6 +1857,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let ((ind,u),_) = dest_ind_family indf' in let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in let arsign = fst (get_arity env0 indf') in + let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in let realnal = match t with | Some (loc,ind',realnal) -> @@ -1874,7 +1867,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = anomaly (Pp.str "Ill-formed 'in' clause in cases"); List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in - LocalAssum (na, build_dependent_inductive env0 indf') + LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf')) ::(List.map2 RelDecl.set_name realnal arsign) in let rec buildrec n = function | [],[] -> [] @@ -2069,7 +2062,7 @@ let constr_of_pat env evdref arsign pat avoid = let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, id :: avoid in - (PatVar (l, name), [local_assum (name, ty)] @ realargs, mkRel 1, ty, + (PatVar (l, name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid) | PatCstr (l,((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in @@ -2110,7 +2103,7 @@ let constr_of_pat env evdref arsign pat avoid = Anonymous -> pat', sign, app, apptype, realargs, n, avoid | Name id -> - let sign = local_assum (alias, lift m ty) :: sign in + let sign = LocalAssum (alias, lift m ty) :: sign in let avoid = id :: avoid in let sign, i, avoid = try @@ -2122,14 +2115,14 @@ let constr_of_pat env evdref arsign pat avoid = (lift 1 app) (* aliased term *) in let neq = eq_id avoid id in - local_def (Name neq, mkRel 0, eq_t) :: sign, 2, neq :: avoid + LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, neq :: avoid with Reduction.NotConvertible -> sign, 1, avoid in (* Mark the equality as a hole *) pat', sign, lift i app, lift i apptype, realargs, n + i, avoid in - let pat', sign, patc, patty, args, z, avoid = typ env (EConstr.of_constr (RelDecl.get_type (List.hd arsign)), List.tl arsign) pat avoid in - pat', (sign, patc, (EConstr.of_constr (RelDecl.get_type (List.hd arsign)), args), pat'), avoid + let pat', sign, patc, patty, args, z, avoid = typ env (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in + pat', (sign, patc, (RelDecl.get_type (List.hd arsign), args), pat'), avoid (* shadows functional version *) @@ -2147,14 +2140,14 @@ match EConstr.kind sigma t with let rels_of_patsign sigma = List.map (fun decl -> match decl with - | LocalDef (na,t',t) when is_topvar sigma (EConstr.of_constr t') -> LocalAssum (na,t) + | LocalDef (na,t',t) when is_topvar sigma t' -> LocalAssum (na,t) | _ -> decl) let vars_of_ctx sigma ctx = let _, y = List.fold_right (fun decl (prev, vars) -> match decl with - | LocalDef (na,t',t) when is_topvar sigma (EConstr.of_constr t') -> + | LocalDef (na,t',t) when is_topvar sigma t' -> prev, (GApp (Loc.ghost, (GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)), @@ -2174,6 +2167,9 @@ let rec is_included x y = if Int.equal i i' then List.for_all2 is_included args args' else false +let lift_rel_context n l = + map_rel_context_with_binders (liftn n) l + (* liftsign is the current pattern's complete signature length. Hence pats is already typed in its full signature. However prevpatterns are in the original one signature per pattern form. @@ -2269,7 +2265,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = match ineqs with | None -> [], arity | Some ineqs -> - [local_assum (Anonymous, ineqs)], lift 1 arity + [LocalAssum (Anonymous, ineqs)], lift 1 arity in let eqs_rels, arity = decompose_prod_n_assum !evdref neqs arity in eqs_rels @ neqs_rels @ rhs_rels', arity @@ -2280,7 +2276,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in let _btype = evd_comb1 (Typing.type_of env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in - let branch_decl = local_def (Name branch_name, lift !i bbody, lift !i btype) in + let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in let branch = let bref = GVar (Loc.ghost, branch_name) in match vars_of_ctx !evdref rhs_rels with @@ -2329,7 +2325,7 @@ let abstract_tomatch env sigma tomatchs tycon = (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, + LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, name :: names, tycon) ([], [], [], tycon) tomatchs in List.rev prev, ctx, tycon @@ -2356,14 +2352,12 @@ let build_dependent_signature env evdref avoid tomatchs arsign = let app_decl = List.hd arsign in (* The matched argument *) let appn = RelDecl.get_name app_decl in let appt = RelDecl.get_type app_decl in - let appt = EConstr.of_constr appt in let argsign = List.rev argsign in (* arguments in application order *) let env', nargeqs, argeqs, refl_args, slift, argsign' = List.fold_left2 (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg decl -> let name = RelDecl.get_name decl in let t = RelDecl.get_type decl in - let t = EConstr.of_constr t in let argt = Retyping.get_type_of env !evdref arg in let eq, refl_arg = if Reductionops.is_conv env !evdref argt t then @@ -2387,7 +2381,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign = make_prime avoid name in (env, succ nargeqs, - (local_assum (Name (eq_id avoid previd), eq)) :: argeqs, + (LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs, refl_arg :: refl_args, pred slift, RelDecl.set_name (Name id) decl :: argsign')) @@ -2401,7 +2395,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign = in let refl_eq = mk_JMeq_refl evdref ty tm in let previd, id = make_prime avoid appn in - ((local_assum (Name (eq_id avoid previd), eq) :: argeqs) :: eqs, + ((LocalAssum (Name (eq_id avoid previd), eq) :: argeqs) :: eqs, succ nargeqs, refl_eq :: refl_args, pred slift, @@ -2417,7 +2411,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign = mk_eq evdref (lift nar tomatch_ty) (mkRel slift) (lift nar tm) in - ([local_assum (Name (eq_id avoid previd), eq)] :: eqs, succ neqs, + ([LocalAssum (Name (eq_id avoid previd), eq)] :: eqs, succ neqs, (mk_eq_refl evdref tomatch_ty tm) :: refl_args, pred slift, (arsign' :: []) :: arsigns)) ([], 0, [], nar, []) tomatchs arsign @@ -2491,9 +2485,9 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let out_tmt na = function NotInd (None,t) -> local_assum (na,t) - | NotInd (Some b, t) -> local_def (na,b,t) - | IsInd (typ,_,_) -> local_assum (na,typ) in + let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) + | NotInd (Some b, t) -> LocalDef (na,b,t) + | IsInd (typ,_,_) -> LocalAssum (na,typ) in let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in let typs = @@ -2566,9 +2560,9 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e (* names of aliases will be recovered from patterns (hence Anonymous *) (* here) *) - let out_tmt na = function NotInd (None,t) -> local_assum (na,t) - | NotInd (Some b,t) -> local_def (na,b,t) - | IsInd (typ,_,_) -> local_assum (na,typ) in + let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) + | NotInd (Some b,t) -> LocalDef (na,b,t) + | IsInd (typ,_,_) -> LocalAssum (na,typ) in let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in let typs = diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9f26ae9ce..3df2d6873 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -47,11 +47,11 @@ val compile_cases : val constr_of_pat : Environ.env -> Evd.evar_map ref -> - Context.Rel.Declaration.t list -> + rel_context -> Glob_term.cases_pattern -> Names.Id.t list -> Glob_term.cases_pattern * - (Context.Rel.Declaration.t list * constr * + (rel_context * constr * (types * constr list) * Glob_term.cases_pattern) * Names.Id.t list @@ -85,7 +85,7 @@ type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (bool * (Name.t * constr * (constr * types))) | NonDepAlias - | Abstract of int * Context.Rel.Declaration.t + | Abstract of int * rel_declaration type tomatch_stack = tomatch_status list @@ -119,6 +119,6 @@ val prepare_predicate : Loc.t -> Environ.env -> Evd.evar_map -> (types * tomatch_type) list -> - Context.Rel.t list -> + rel_context list -> constr option -> 'a option -> (Evd.evar_map * Names.name list * constr) list diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 91f53a886..8794f238b 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -18,10 +18,10 @@ open CErrors open Util open Names open Term +open Environ open EConstr open Vars open Reductionops -open Environ open Typeops open Pretype_errors open Classops @@ -127,10 +127,6 @@ let lift_args n sign = in liftrec (List.length sign) sign -let local_assum (na, t) = - let open Context.Rel.Declaration in - LocalAssum (na, EConstr.Unsafe.to_constr t) - let mu env evdref t = let rec aux v = let v' = hnf env !evdref v in @@ -159,7 +155,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) let subco () = subset_coerce env evdref x y in let dest_prod c = match Reductionops.splay_prod_n env (!evdref) 1 c with - | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, EConstr.of_constr t), c + | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, t), c | _ -> raise NoSubtacCoercion in let coerce_application typ typ' c c' l l' = @@ -212,7 +208,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) let name' = Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env)) in - let env' = push_rel (local_assum (name', a')) env in + let env' = push_rel (LocalAssum (name', a')) env in let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) let coec1 = app_opt env' evdref c1 (mkRel 1) in @@ -260,7 +256,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) | _ -> raise NoSubtacCoercion in let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in - let env' = push_rel (local_assum (Name Namegen.default_dependent_ident, a)) env in + let env' = push_rel (LocalAssum (Name Namegen.default_dependent_ident, a)) env in let c2 = coerce_unify env' b b' in match c1, c2 with | None, None -> None @@ -489,7 +485,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = | Anonymous -> Name Namegen.default_dependent_ident | _ -> name in let open Context.Rel.Declaration in - let env1 = push_rel (local_assum (name,u1)) env in + let env1 = push_rel (LocalAssum (name,u1)) env in let (evd', v1) = inh_conv_coerce_to_fail loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 55612aa66..cad21543b 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -136,14 +136,6 @@ let make_renaming ids = function end | _ -> dummy_constr -let local_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - let to_fix (idx, (nas, cs, ts)) = let inj = EConstr.of_constr in (idx, (nas, Array.map inj cs, Array.map inj ts)) @@ -273,15 +265,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels sorec ctx env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (Environ.push_rel (local_assum (na2,c2)) env) + sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (Environ.push_rel (local_assum (na2,c2)) env) + sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na1,na2,t2)::ctx) (Environ.push_rel (local_def (na2,c2,t2)) env) + sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> @@ -290,12 +282,12 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let n = Context.Rel.length ctx_b2 in let n' = Context.Rel.length ctx_b2' in if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then - let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,EConstr.of_constr t)::l in + let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in let ctx_br = List.fold_left f ctx ctx_b2 in let ctx_br' = List.fold_left f ctx ctx_b2' in let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in - sorec ctx_br' (Environ.push_rel_context ctx_b2' env) - (sorec ctx_br (Environ.push_rel_context ctx_b2 env) + sorec ctx_br' (push_rel_context ctx_b2' env) + (sorec ctx_br (push_rel_context ctx_b2 env) (sorec ctx env subst a1 a2) b1 b2) b1' b2' else raise PatternMatchingFailure @@ -388,21 +380,21 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2)) | _ -> assert false in - let env' = Environ.push_rel (local_assum (x,c1)) env in + let env' = EConstr.push_rel (LocalAssum (x,c1)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | Prod (x,c1,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkProd (x, c1, c2)) | _ -> assert false in - let env' = Environ.push_rel (local_assum (x,c1)) env in + let env' = EConstr.push_rel (LocalAssum (x,c1)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | LetIn (x,c1,t,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2)) | _ -> assert false in - let env' = Environ.push_rel (local_def (x,c1,t)) env in + let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> let topdown = true in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3ae2e35e6..f5cab070e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -11,12 +11,12 @@ open Util open Names open Term open Termops +open Environ open EConstr open Vars open CClosure open Reduction open Reductionops -open Environ open Recordops open Evarutil open Evardefine @@ -58,12 +58,12 @@ let eval_flexible_term ts env evd c = | Rel n -> (try match lookup_rel n env with | RelDecl.LocalAssum _ -> None - | RelDecl.LocalDef (_,v,_) -> Some (lift n (EConstr.of_constr v)) + | RelDecl.LocalDef (_,v,_) -> Some (lift n v) with Not_found -> None) | Var id -> (try if is_transparent_variable ts id then - Option.map EConstr.of_constr (env |> lookup_named id |> NamedDecl.get_value) + env |> lookup_named id |> NamedDecl.get_value else None with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) @@ -404,7 +404,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let eta env evd onleft sk term sk' term' = assert (match sk with [] -> true | _ -> false); let (na,c1,c'1) = destLambda evd term in - let c = EConstr.to_constr evd c1 in + let c = nf_evar evd c1 in let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in @@ -612,8 +612,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> evar_conv_x ts env i CUMUL t2 t1)]); (fun i -> evar_conv_x ts env i CONV b1 b2); (fun i -> - let b = EConstr.to_constr i b1 in - let t = EConstr.to_constr i t1 in + let b = nf_evar i b1 in + let t = nf_evar i t1 in let na = Nameops.name_max na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] @@ -730,7 +730,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> - let c = EConstr.to_constr i c1 in + let c = nf_evar i c1 in let na = Nameops.name_max na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] @@ -789,7 +789,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> - let c = EConstr.to_constr i c1 in + let c = nf_evar i c1 in let na = Nameops.name_max n1 n2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 5831d3191..faf34baf7 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -11,10 +11,10 @@ open Pp open Names open Term open Termops +open Environ open EConstr open Vars open Namegen -open Environ open Evd open Evarutil open Pretype_errors @@ -22,25 +22,20 @@ open Sigma.Notations module RelDecl = Context.Rel.Declaration -let nlocal_assum (na, t) = - let open Context.Named.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = let evd = Sigma.Unsafe.of_evar_map evd in let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in (Sigma.to_evar_map evd, evk) let env_nf_evar sigma env = - let nf_evar c = EConstr.Unsafe.to_constr (nf_evar sigma (EConstr.of_constr c)) in + let nf_evar c = nf_evar sigma c in process_rel_context (fun d e -> push_rel (RelDecl.map_constr nf_evar d) e) env let env_nf_betaiotaevar sigma env = process_rel_context (fun d e -> - push_rel (RelDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma (EConstr.of_constr c))) d) e) env + push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma c) d) e) env (****************************************) (* Operations on value/type constraints *) @@ -93,7 +88,7 @@ let define_pure_evar_as_product evd evk = (Sigma.to_evar_map evd1, e) in let evd2,rng = - let newenv = push_named (nlocal_assum (id, dom)) evenv in + let newenv = push_named (LocalAssum (id, dom)) evenv in let src = evar_source evk evd1 in let filter = Filter.extend 1 (evar_filter evi) in if is_prop_sort s then @@ -146,7 +141,7 @@ let define_pure_evar_as_lambda env evd evk = let avoid = ids_of_named_context (evar_context evi) in let id = next_name_away_with_default_using_types "x" na avoid (EConstr.Unsafe.to_constr (Reductionops.whd_evar evd dom)) in - let newenv = push_named (nlocal_assum (id, dom)) evenv in + let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = evar_source evk evd1 in let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 3235c2505..ff4736528 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -23,14 +23,6 @@ open Evarutil open Pretype_errors open Sigma.Notations -let nlocal_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - Context.Named.Declaration.LocalAssum (na, inj t) - -let nlocal_def (na, b, t) = - let inj = EConstr.Unsafe.to_constr in - Context.Named.Declaration.LocalDef (na, inj b, inj t) - let normalize_evar evd ev = match EConstr.kind evd (mkEvar ev) with | Evar (evk,args) -> (evk,args) @@ -264,7 +256,6 @@ let compute_var_aliases sign sigma = let id = get_id decl in match decl with | LocalDef (_,t,_) -> - let t = EConstr.of_constr t in (match EConstr.kind sigma t with | Var id' -> let aliases_of_id = @@ -281,8 +272,6 @@ let compute_rel_aliases var_aliases rels sigma = (n-1, match decl with | LocalDef (_,t,u) -> - let t = EConstr.of_constr t in - let u = EConstr.of_constr u in (match EConstr.kind sigma t with | Var id' -> let aliases_of_n = @@ -338,7 +327,6 @@ let extend_alias sigma decl (var_aliases,rel_aliases) = let rel_aliases = match decl with | LocalDef(_,t,_) -> - let t = EConstr.of_constr t in (match EConstr.kind sigma t with | Var id' -> let aliases_of_binder = @@ -530,7 +518,7 @@ let solve_pattern_eqn env sigma l c = (* Rem: if [a] links to a let-in, do as if it were an assumption *) | Rel n -> let open Context.Rel.Declaration in - let d = map_constr (CVars.lift n) (lookup_rel n env) in + let d = map_constr (lift n) (lookup_rel n env) in mkLambda_or_LetIn d c' | Var id -> let d = lookup_named id env in mkNamedLambda_or_LetIn d c' @@ -556,6 +544,7 @@ let solve_pattern_eqn env sigma l c = let make_projectable_subst aliases sigma evi args = let sign = evar_filtered_context evi in + let sign = List.map (fun d -> map_named_decl EConstr.of_constr d) sign in let evar_aliases = compute_var_aliases sign sigma in let (_,full_subst,cstr_subst) = List.fold_right @@ -571,7 +560,7 @@ let make_projectable_subst aliases sigma evi args = | _ -> cstrs in (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs) | LocalDef (id,c,_), a::rest -> - (match EConstr.kind sigma (EConstr.of_constr c) with + (match EConstr.kind sigma c with | Var id' -> let idc = normalize_alias_var sigma evar_aliases id' in let sub = try Id.Map.find idc all with Not_found -> [] in @@ -646,19 +635,17 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in let id = next_name_away na avoid in let evd,t_in_sign = - let t_in_env = EConstr.of_constr t_in_env in let s = Retyping.get_sort_of env evd t_in_env in let evd,ty_t_in_sign = refresh_universes ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env in let evd,d' = match d with - | LocalAssum _ -> evd, nlocal_assum (id,t_in_sign) + | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign) | LocalDef (_,b,_) -> - let b = EConstr.of_constr b in let evd,b = define_evar_from_virtual_equation define_fun env evd src b t_in_sign sign filter inst_in_env in - evd, nlocal_def (id,b,t_in_sign) in + evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in (push_named_context_val d' sign, Filter.extend 1 filter, (mkRel 1)::(List.map (lift 1) inst_in_env), (mkRel 1)::(List.map (lift 1) inst_in_sign), @@ -1238,9 +1225,11 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *) let evienv = Evd.evar_env evi in let ctx1, i = Reduction.dest_arity evienv evi.evar_concl in + let ctx1 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx1 in let evi2 = Evd.find evd evk2 in let evi2env = Evd.evar_env evi2 in let ctx2, j = Reduction.dest_arity evi2env evi2.evar_concl in + let ctx2 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx2 in let ui, uj = univ_of_sort i, univ_of_sort j in if i == j || Evd.check_eq evd ui uj then (* Shortcut, i = j *) @@ -1397,7 +1386,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = (* No unique projection but still restrict to where it is possible *) (* materializing is necessary, but is restricting useful? *) let ty = find_solution_type (evar_filtered_env evi) sols in - let ty' = instantiate_evar_array evi (EConstr.of_constr ty) argsv in + let ty' = instantiate_evar_array evi ty argsv in let (evd,evar,(evk',argsv' as ev')) = materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in let ts = expansions_of_var evd aliases t in diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index d09686f6e..3fc569fc4 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -64,8 +64,8 @@ let proceed_with_occurrences f occs x = let map_named_declaration_with_hyploc f hyploc acc decl = let open Context.Named.Declaration in let f acc typ = - let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc (EConstr.of_constr typ) in - acc, EConstr.Unsafe.to_constr typ + let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc typ in + acc, typ in match decl,hyploc with | LocalAssum (id,_), InHypValueOnly -> diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 3d2ebb72d..e3d3b74f1 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -51,7 +51,7 @@ val replace_term_occ_decl_modulo : evar_map -> (occurrences * hyp_location_flag) or_like_first -> 'a testing_function -> (unit -> constr) -> - Context.Named.Declaration.t -> Context.Named.Declaration.t + named_declaration -> named_declaration (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC), @@ -63,7 +63,7 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first -> closed [c] at positions [occl] by [Rel 1] in [decl]. *) val subst_closed_term_occ_decl : env -> evar_map -> (occurrences * hyp_location_flag) or_like_first -> - constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map + constr -> named_declaration -> named_declaration * evar_map (** Miscellaneous *) val error_invalid_occurrence : int list -> 'a diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index c00ceb02e..3191a58ff 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -371,7 +371,7 @@ let make_case_or_project env sigma indf ci pred c branches = | LocalAssum (na, t) -> let t = mkProj (Projection.make ps.(i) true, c) in (i + 1, t :: subst) - | LocalDef (na, b, t) -> (i, Vars.substl subst (EConstr.of_constr b) :: subst)) + | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) ctx (0, []) in Vars.substl subst br diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 26e23be23..954aa6a94 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -121,19 +121,10 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with | Var id -> VarRef id | _ -> anomaly (Pp.str "Not a rigid reference") -let local_assum (na, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - let pattern_of_constr env sigma t = let open EConstr in let rec pattern_of_constr env t = + let open Context.Rel.Declaration in match EConstr.kind sigma t with | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) @@ -143,11 +134,11 @@ let pattern_of_constr env sigma t = | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c, - pattern_of_constr (push_rel (local_def (na,c,t)) env) b) + pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) | Prod (na,c,b) -> PProd (na,pattern_of_constr env c, - pattern_of_constr (push_rel (local_assum (na, c)) env) b) + pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c, - pattern_of_constr (push_rel (local_assum (na, c)) env) b) + pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match match EConstr.kind sigma f with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4660978df..2470decdd 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,10 +28,10 @@ open Names open Evd open Term open Termops +open Environ open EConstr open Vars open Reductionops -open Environ open Type_errors open Typeops open Typing @@ -70,16 +70,6 @@ open Inductiveops (************************************************************************) -let local_assum (na, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - module ExtraEnv = struct @@ -94,7 +84,7 @@ let get_extra env = let ids = List.map get_id (named_context env) in let avoid = List.fold_right Id.Set.add ids Id.Set.empty in Context.Rel.fold_outside push_rel_decl_to_named_context - (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) let make_env env = { env = env; extra = lazy (get_extra env) } let rel_context env = rel_context env.env @@ -116,7 +106,7 @@ let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in - let inst_vars = List.map (get_id %> EConstr.mkVar) (named_context env.env) in + let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in let (subst, vsubst, _, nc) = Lazy.force env.extra in let typ' = subst2 subst vsubst typ in @@ -128,7 +118,7 @@ let e_new_evar env evdref ?src ?naming typ = e let push_rec_types (lna,typarray,_) env = - let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt end @@ -434,7 +424,6 @@ let pretype_id pretype k0 loc env evdref lvar id = (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in - let typ = EConstr.of_constr typ in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> let env = ltac_interp_name_env k0 lvar env in @@ -468,7 +457,7 @@ let pretype_id pretype k0 loc env evdref lvar id = end; (* Check if [id] is a section or goal variable *) try - { uj_val = mkVar id; uj_type = EConstr.of_constr (NamedDecl.get_type (lookup_named id env)) } + { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found ~loc id @@ -511,7 +500,7 @@ let pretype_ref loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try make_judge (mkVar id) (EConstr.of_constr (NamedDecl.get_type (lookup_named id env))) + (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env)) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal @@ -614,14 +603,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre [] -> ctxt | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let dcl = local_assum (na, ty'.utj_val) in - let dcl' = local_assum (ltac_interp_name lvar na,ty'.utj_val) in + let dcl = LocalAssum (na, ty'.utj_val) in + let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in - let dcl = local_def (na, bd'.uj_val, ty'.utj_val) in - let dcl' = local_def (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in + let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in + let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = @@ -793,7 +782,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = local_assum (name, j.utj_val) in + let var = LocalAssum (name, j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in @@ -809,7 +798,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = pretype_type empty_valcon env evdref lvar c2 in { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = local_assum (name, j.utj_val) in + let var = LocalAssum (name, j.utj_val) in let env' = push_rel var env in pretype_type empty_valcon env' evdref lvar c2 in @@ -837,7 +826,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = local_def (name, j.uj_val, t) in + let var = LocalDef (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in @@ -861,6 +850,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre user_err ~loc:loc (str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign, record = + let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in match get_projections env.ExtraEnv.env indf with | None -> List.map2 set_name (List.rev nal) cs.cs_args, false @@ -870,7 +860,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | na :: names, (LocalAssum (_,t) :: l) -> let t = EConstr.of_constr t in let proj = Projection.make ps.(cs.cs_nargs - k) true in - local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) + LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) :: aux (n+1) (k + 1) names l | na :: names, (decl :: l) -> set_name na decl :: aux (n+1) k names l @@ -896,6 +886,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre else arsgn in let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in + let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let nar = List.length arsgn in (match po with | Some p -> @@ -903,6 +894,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 psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) + let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs) @@ -956,6 +948,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let nar = List.length arsgn in let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in + let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let pred,p = match po with | Some p -> let env_p = push_rel_context psign env in @@ -978,17 +971,18 @@ 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 cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in let csgn = if not !allow_anonymous_refs then - List.map (set_name Anonymous) cs.cs_args + List.map (set_name Anonymous) cs_args else List.map (map_name (function Name _ as n -> n | Anonymous -> Name Namegen.default_non_dependent_ident)) - cs.cs_args + cs_args in let env_c = push_rel_context csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in - it_mkLambda_or_LetIn bj.uj_val cs.cs_args in + it_mkLambda_or_LetIn bj.uj_val cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = @@ -1060,12 +1054,10 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - let t' = EConstr.of_constr t' in if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try let t' = env |> lookup_named id |> NamedDecl.get_type in - let t' = EConstr.of_constr t' in if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err ~loc (str "Cannot interpret " ++ diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bc5c629f4..a1585ef52 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -13,9 +13,9 @@ open Term open Termops open Univ open Evd +open Environ open EConstr open Vars -open Environ open Context.Rel.Declaration exception Elimconst @@ -609,14 +609,6 @@ let pr_state (tm,sk) = let pr c = Termops.print_constr c in h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk) -let local_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - (*************************************) (*** Reduction Functions Operators ***) (*************************************) @@ -851,12 +843,12 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = match c0 with | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA -> (match lookup_rel n env with - | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n (EConstr.of_constr body), stack) + | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack) | _ -> fold ()) | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) -> (match lookup_named id env with | LocalDef (_,body,_) -> - whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (EConstr.of_constr body, stack) + whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack) | _ -> fold ()) | Evar ev -> fold () | Meta ev -> @@ -958,7 +950,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> - let env' = push_rel (local_assum (na, t)) env in + let env' = push_rel (LocalAssum (na, t)) env in let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with | App (f,cl) -> @@ -1468,7 +1460,7 @@ let splay_prod env sigma = let t = whd_all env sigma c in match EConstr.kind sigma t with | Prod (n,a,c0) -> - decrec (push_rel (local_assum (n,a)) env) + decrec (push_rel (LocalAssum (n,a)) env) (bind_assum (n,a)::m) c0 | _ -> m,t in @@ -1479,7 +1471,7 @@ let splay_lam env sigma = let t = whd_all env sigma c in match EConstr.kind sigma t with | Lambda (n,a,c0) -> - decrec (push_rel (local_assum (n,a)) env) + decrec (push_rel (LocalAssum (n,a)) env) (bind_assum (n,a)::m) c0 | _ -> m,t in @@ -1490,11 +1482,11 @@ let splay_prod_assum env sigma = let t = whd_allnolet env sigma c in match EConstr.kind sigma t with | Prod (x,t,c) -> - prodec_rec (push_rel (local_assum (x,t)) env) - (Context.Rel.add (local_assum (x,t)) l) c + prodec_rec (push_rel (LocalAssum (x,t)) env) + (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> - prodec_rec (push_rel (local_def (x,b,t)) env) - (Context.Rel.add (local_def (x,b,t)) l) c + prodec_rec (push_rel (LocalDef (x,b,t)) env) + (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> let t' = whd_all env sigma t in @@ -1515,8 +1507,8 @@ let splay_prod_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match EConstr.kind sigma (whd_all env sigma c) with | Prod (n,a,c0) -> - decrec (push_rel (local_assum (n,a)) env) - (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0 + decrec (push_rel (LocalAssum (n,a)) env) + (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 | _ -> invalid_arg "splay_prod_n" in decrec env n Context.Rel.empty @@ -1525,8 +1517,8 @@ let splay_lam_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match EConstr.kind sigma (whd_all env sigma c) with | Lambda (n,a,c0) -> - decrec (push_rel (local_assum (n,a)) env) - (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0 + decrec (push_rel (LocalAssum (n,a)) env) + (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 | _ -> invalid_arg "splay_lam_n" in decrec env n Context.Rel.empty @@ -1566,8 +1558,8 @@ let find_conclusion env sigma = let rec decrec env c = let t = whd_all env sigma c in match EConstr.kind sigma t with - | Prod (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0 - | Lambda (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0 + | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 + | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 | t -> t in decrec env diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index dcc11cfcf..15ddeb15c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -217,10 +217,10 @@ val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts val sort_of_arity : env -> evar_map -> constr -> sorts -val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr -val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr +val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr +val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_prod_assum : - env -> evar_map -> constr -> Context.Rel.t * constr + env -> evar_map -> constr -> rel_context * constr type 'a miota_args = { mP : constr; (** the result type *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a9529d560..bb1b2901e 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -50,14 +50,6 @@ let anomaly_on_error f x = try f x with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e) -let local_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - let get_type_from_constraints env sigma t = if isEvar sigma (fst (decompose_app_vect sigma t)) then match @@ -84,13 +76,13 @@ let rec subst_type env sigma typ = function let sort_of_atomic_type env sigma ft args = let rec concl_of_arity env n ar args = match EConstr.kind sigma (whd_all env sigma ar), args with - | Prod (na, t, b), h::l -> concl_of_arity (push_rel (local_def (na, lift n h, t)) env) (n + 1) b l + | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l | Sort s, [] -> s | _ -> retype_error NotASort in concl_of_arity env 0 ft (Array.to_list args) let type_of_var env id = - try EConstr.of_constr (NamedDecl.get_type (lookup_named id env)) + try NamedDecl.get_type (lookup_named id env) with Not_found -> retype_error (BadVariable id) let decomp_sort env sigma t = @@ -105,7 +97,7 @@ let retype ?(polyprop=true) sigma = (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 + let ty = RelDecl.get_type (lookup_rel n env) in lift n ty | Var id -> type_of_var env id | Const cst -> EConstr.of_constr (rename_type_of_constant env cst) @@ -128,9 +120,9 @@ let retype ?(polyprop=true) sigma = | Prod _ -> whd_beta sigma (applist (t, [c])) | _ -> t) | Lambda (name,c1,c2) -> - mkProd (name, c1, type_of (push_rel (local_assum (name,c1)) env) c2) + mkProd (name, c1, type_of (push_rel (LocalAssum (name,c1)) env) c2) | LetIn (name,b,c1,c2) -> - subst1 b (type_of (push_rel (local_def (name,b,c1)) env) c2) + subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2) | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) | App(f,args) when is_template_polymorphic env sigma f -> @@ -153,7 +145,7 @@ let retype ?(polyprop=true) sigma = | Sort (Prop c) -> type1_sort | Sort (Type u) -> Type (Univ.super u) | Prod (name,t,c2) -> - (match (sort_of env t, sort_of (push_rel (local_assum (name,t)) env) c2) with + (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with | _, (Prop Null as s) -> s | Prop _, (Prop Pos as s) -> s | Type _, (Prop Pos as s) when is_impredicative_set env -> s @@ -174,7 +166,7 @@ let retype ?(polyprop=true) sigma = | Sort (Prop c) -> InType | Sort (Type u) -> InType | Prod (name,t,c2) -> - let s2 = sort_family_of (push_rel (local_assum (name,t)) env) c2 in + let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 | App(f,args) when is_template_polymorphic env sigma f -> @@ -249,7 +241,7 @@ let sorts_of_context env evc ctxt = | [] -> env,[] | d :: ctxt -> let env,sorts = aux ctxt in - let s = get_sort_of env evc (EConstr.of_constr (RelDecl.get_type d)) in + let s = get_sort_of env evc (RelDecl.get_type d) in (push_rel d env,s::sorts) in snd (aux ctxt) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index ce9e1635f..25129db1c 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -44,7 +44,7 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> val type_of_global_reference_knowing_conclusion : env -> evar_map -> constr -> types -> evar_map * types -val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list +val sorts_of_context : env -> evar_map -> rel_context -> sorts list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 4abfc26fc..9f3f3c7e5 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -14,11 +14,11 @@ open Term open Libnames open Globnames open Termops +open Environ open EConstr open Vars open Find_subterm open Namegen -open Environ open CClosure open Reductionops open Cbv @@ -60,7 +60,7 @@ let is_evaluable env = function let value_of_evaluable_ref env evref u = match evref with | EvalConstRef con -> - (try constant_value_in env (con,u) + EConstr.of_constr (try constant_value_in env (con,u) with NotEvaluableConst IsProj -> raise (Invalid_argument "value_of_evaluable_ref")) | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get @@ -115,9 +115,9 @@ let unsafe_reference_opt_value env sigma eval = | Declarations.Def c -> Some (EConstr.of_constr (Mod_subst.force_constr c)) | _ -> None) | EvalVar id -> - env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr + env |> lookup_named id |> NamedDecl.get_value | EvalRel n -> - env |> lookup_rel n |> RelDecl.get_value |> Option.map (EConstr.of_constr %> lift n) + env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n) | EvalEvar ev -> match EConstr.kind sigma (mkEvar ev) with | Evar _ -> None @@ -127,9 +127,9 @@ let reference_opt_value env sigma eval u = match eval with | EvalConst cst -> Option.map EConstr.of_constr (constant_opt_value_in env (cst,u)) | EvalVar id -> - env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr + env |> lookup_named id |> NamedDecl.get_value | EvalRel n -> - env |> lookup_rel n |> RelDecl.get_value |> Option.map (EConstr.of_constr %> lift n) + env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n) | EvalEvar ev -> match EConstr.kind sigma (mkEvar ev) with | Evar _ -> None @@ -146,11 +146,11 @@ let reference_value env sigma c u = (* One reuses the name of the function after reduction of the fixpoint *) type constant_evaluation = - | EliminationFix of int * int * (int * (int * EConstr.t) list * int) + | EliminationFix of int * int * (int * (int * constr) list * int) | EliminationMutualFix of int * evaluable_reference * ((int*evaluable_reference) option array * - (int * (int * EConstr.t) list * int)) + (int * (int * constr) list * int)) | EliminationCases of int | EliminationProj of int | NotAnElimination @@ -261,22 +261,13 @@ let invert_name labs l na0 env sigma ref = function [compute_consteval_mutual_fix] only one by one, until finding the last one before the Fix if the latter is mutually defined *) -let local_assum (na, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - let compute_consteval_direct env sigma ref = let rec srec env n labs onlyproj c = let c',l = whd_betadeltazeta_stack env sigma c in match EConstr.kind sigma c' with | Lambda (id,t,g) when List.is_empty l && not onlyproj -> - srec (push_rel (local_assum (id,t)) env) (n+1) (t::labs) onlyproj g + let open Context.Rel.Declaration in + srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) onlyproj g | Fix fix when not onlyproj -> (try check_fix_reversibility sigma labs l fix with Elimconst -> NotAnElimination) @@ -295,7 +286,8 @@ let compute_consteval_mutual_fix env sigma ref = let nargs = List.length l in match EConstr.kind sigma c' with | Lambda (na,t,g) when List.is_empty l -> - srec (push_rel (local_assum (na,t)) env) (minarg+1) (t::labs) ref g + let open Context.Rel.Declaration in + srec (push_rel (LocalAssum (na,t)) env) (minarg+1) (t::labs) ref g | Fix ((lv,i),(names,_,_)) -> (* Last known constant wrapping Fix is ref = [labs](Fix l) *) (match compute_consteval_direct env sigma ref with @@ -386,7 +378,7 @@ let make_elim_fun (names,(nbfix,lv,n)) u largs = (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: do so that the reduction uses this extra information *) -let dummy = Constr.mkProp +let dummy = mkProp let vfx = Id.of_string "_expanded_fix_" let vfun = Id.of_string "_eliminator_function_" let venv = let open Context.Named.Declaration in @@ -405,7 +397,7 @@ let substl_with_function subst sigma constr = match v.(i-k-1) with | (fx, Some (min, ref)) -> let sigma = Sigma.Unsafe.of_evar_map !evd in - let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma (EConstr.of_constr dummy) in + let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in let sigma = Sigma.to_evar_map sigma in evd := sigma; minargs := Evar.Map.add evk min !minargs; @@ -466,7 +458,7 @@ let substl_checking_arity env subst sigma c = in nf_fix body -type fix_reduction_result = NotReducible | Reduced of (EConstr.t * EConstr.t list) +type fix_reduction_result = NotReducible | Reduced of (constr * constr list) let reduce_fix whdfun sigma fix stack = match fix_recarg fix (Stack.append_app_list stack Stack.empty) with @@ -557,9 +549,9 @@ let match_eval_ref_value env sigma constr = | Const (sp, u) when is_evaluable env (EvalConstRef sp) -> Some (EConstr.of_constr (constant_value_in env (sp, u))) | Var id when is_evaluable env (EvalVarRef id) -> - env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr + env |> lookup_named id |> NamedDecl.get_value | Rel n -> - env |> lookup_rel n |> RelDecl.get_value |> Option.map (EConstr.of_constr %> lift n) + env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n) | _ -> None let special_red_case env sigma whfun (ci, p, c, lf) = @@ -625,12 +617,12 @@ let whd_nothing_for_iota env sigma s = | Rel n -> let open Context.Rel.Declaration in (match lookup_rel n env with - | LocalDef (_,body,_) -> whrec (lift n (EConstr.of_constr body), stack) + | LocalDef (_,body,_) -> whrec (lift n body, stack) | _ -> s) | Var id -> let open Context.Named.Declaration in (match lookup_named id env with - | LocalDef (_,body,_) -> whrec (EConstr.of_constr body, stack) + | LocalDef (_,body,_) -> whrec (body, stack) | _ -> s) | Evar ev -> s | Meta ev -> @@ -834,7 +826,8 @@ let try_red_product env sigma c = | _ -> simpfun (mkApp (redrec env f, l))) | Cast (c,_,_) -> redrec env c | Prod (x,a,b) -> - mkProd (x, a, redrec (push_rel (local_assum (x, a)) env) b) + let open Context.Rel.Declaration in + mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b) | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t) | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf)) | Proj (p, c) -> @@ -1053,7 +1046,7 @@ let substlin env sigma evalref n (nowhere_except_in,locs) c = let maxocc = List.fold_right max locs 0 in let pos = ref n in assert (List.for_all (fun x -> x >= 0) locs); - let value u = EConstr.of_constr (value_of_evaluable_ref env evalref u) in + let value u = value_of_evaluable_ref env evalref u in let rec substrec () c = if nowhere_except_in && !pos > maxocc then c else @@ -1192,7 +1185,7 @@ let reduce_to_ind_gen allow_product env sigma t = | Prod (n,ty,t') -> let open Context.Rel.Declaration in if allow_product then - elimrec (push_rel (local_assum (n,ty)) env) t' ((local_assum (n,ty))::l) + elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) else user_err (str"Not an inductive definition.") | _ -> @@ -1270,7 +1263,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = | Prod (n,ty,t') -> if allow_product then let open Context.Rel.Declaration in - elimrec (push_rel (local_assum (n,t)) env) t' ((local_assum (n,ty))::l) + elimrec (push_rel (LocalAssum (n,t)) env) t' ((LocalAssum (n,ty))::l) else error_cannot_recognize ref | _ -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 50ae66eb0..ce570ee12 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -300,6 +300,7 @@ let build_subclasses ~check env sigma glob pri = | Some (Backward, _) -> None | Some (Forward, pri') -> let proj = Option.get proj in + let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in if check && check_instance env sigma (EConstr.of_constr body) then None else diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e95aba695..0c30296d3 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -67,7 +67,7 @@ val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses * val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses (** Just return None if not a class *) -val class_of_constr : evar_map -> EConstr.constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option +val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * (typeclass puniverses * constr list)) option val instance_impl : instance -> global_reference diff --git a/pretyping/typing.ml b/pretyping/typing.ml index e6f1e46b6..bdd3663d1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -12,9 +12,9 @@ open Pp open CErrors open Util open Term +open Environ open EConstr open Vars -open Environ open Reductionops open Inductive open Inductiveops @@ -23,14 +23,6 @@ open Arguments_renaming open Pretype_errors open Context.Rel.Declaration -let local_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - let push_rec_types pfix env = let (i, c, t) = pfix in let inj c = EConstr.Unsafe.to_constr c in @@ -101,14 +93,15 @@ let max_sort l = let e_is_correct_arity env evdref c pj ind specif params = let arsign = make_arity_signature env true (make_ind_family (ind,params)) in + let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in let allowed_sorts = elim_sorts specif in let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in let rec srec env pt ar = let pt' = whd_all env !evdref pt in match EConstr.kind !evdref pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error (); - srec (push_rel (local_assum (na1,a1)) env) t ar' + if not (Evarconv.e_cumul env evdref a1 a1') then error (); + srec (push_rel (LocalAssum (na1,a1)) env) t ar' | Sort s, [] -> if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () @@ -326,14 +319,14 @@ let rec execute env evdref cstr = | Lambda (name,c1,c2) -> let j = execute env evdref c1 in let var = e_type_judgment env evdref j in - let env1 = push_rel (local_assum (name, var.utj_val)) env in + let env1 = push_rel (LocalAssum (name, var.utj_val)) env in let j' = execute env1 evdref c2 in judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> let j = execute env evdref c1 in let varj = e_type_judgment env evdref j in - let env1 = push_rel (local_assum (name, varj.utj_val)) env in + let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in let j' = execute env1 evdref c2 in let varj' = e_type_judgment env1 evdref j' in judge_of_product env name varj varj' @@ -343,7 +336,7 @@ let rec execute env evdref cstr = let j2 = execute env evdref c2 in let j2 = e_type_judgment env evdref j2 in let _ = e_judge_of_cast env evdref j1 DEFAULTcast j2 in - let env1 = push_rel (local_def (name, j1.uj_val, j2.utj_val)) env in + let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in let j3 = execute env1 evdref c3 in judge_of_letin env name j1 j2 j3 diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 04cc4253e..0d6dcffc1 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -14,10 +14,10 @@ open Util open Names open Term open Termops +open Environ open EConstr open Vars open Namegen -open Environ open Evd open Reduction open Reductionops @@ -91,7 +91,6 @@ let abstract_scheme env evd c l lname_typ = (fun (t,evd) (locc,a) decl -> let na = RelDecl.get_name decl in let ta = RelDecl.get_type decl in - let ta = EConstr.of_constr ta in let na = match EConstr.kind evd a with Var id -> Name id | _ -> na in (* [occur_meta ta] test removed for support of eelim/ecase but consequences are unclear... @@ -1627,6 +1626,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let likefirst = clause_with_generic_occurrences occs in let mkvarid () = EConstr.mkVar id in let compute_dependency _ d (sign,depdecls) = + let d = map_named_decl EConstr.of_constr d in let hyp = NamedDecl.get_id d in match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> @@ -1634,7 +1634,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = | AllOccurrences, InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in - if Context.Named.Declaration.equal Constr.equal d newdecl + if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl && not (indirectly_dependent sigma c d depdecls) then if check_occs && not (in_every_hyp occs) @@ -1688,7 +1688,7 @@ type abstraction_request = type 'r abstraction_result = Names.Id.t * named_context_val * - Context.Named.Declaration.t list * Names.Id.t option * + named_declaration list * Names.Id.t option * types * (constr, 'r) Sigma.sigma option let make_abstraction env evd ccl abs = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 41dcb8ed3..6760283d2 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -82,7 +82,7 @@ val finish_evar_resolution : ?flags:Pretyping.inference_flags -> type 'r abstraction_result = Names.Id.t * named_context_val * - Context.Named.Declaration.t list * Names.Id.t option * + named_declaration list * Names.Id.t option * types * (constr, 'r) Sigma.sigma option val make_abstraction : env -> 'r Sigma.t -> constr -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 93970512d..64c7c0ba5 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -71,11 +71,11 @@ let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref = let typ = Global.type_of_global_unsafe ref in + let typ = EConstr.of_constr typ in let typ = 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 Term.it_mkProd_or_LetIn ccl ctx + let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ + in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in let env = Global.env () in @@ -85,7 +85,7 @@ let print_ref reduce ref = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () in - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ Printer.pr_universe_ctx sigma univs) (********************************) diff --git a/proofs/goal.ml b/proofs/goal.ml index 410e738de..9046f4534 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -155,6 +155,7 @@ module V82 = struct with Not_found -> true in Environ.fold_named_context_reverse (fun t decl -> if is_proof_var decl then + let decl = Termops.map_named_decl EConstr.of_constr decl in mkNamedProd_or_LetIn decl t else t diff --git a/proofs/logic.ml b/proofs/logic.ml index 59ce8ffa6..a31cadd88 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -174,12 +174,14 @@ let reorder_context env sigma sign ord = step ord ords sign mt_q [] let reorder_val_context env sigma sign ord = + let open EConstr in val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) let check_decl_position env sigma sign d = + let open EConstr in let x = NamedDecl.get_id d in let needed = global_vars_set_of_decl env sigma d in let deps = dependency_closure env sigma (named_context_of_val sign) needed in @@ -266,6 +268,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = else moverec first' middle' right in + let open EConstr in if toleft then let right = List.fold_right push_named_context_val right empty_named_context_val in @@ -279,6 +282,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = right left let move_hyp_in_named_context sigma hfrom hto sign = + let open EConstr in let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in move_hyp sigma toleft (left,declfrom,right) hto @@ -507,7 +511,7 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in - let b = Option.map EConstr.of_constr (NamedDecl.get_value d) in + let b = NamedDecl.get_value d in let env = Global.env() in let reorder = ref [] in let sign' = @@ -515,14 +519,14 @@ let convert_hyp check sign sigma d = (fun _ d' _ -> let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in let env = Global.env_of_context sign in - if check && not (is_conv env sigma (EConstr.of_constr (NamedDecl.get_type d)) (EConstr.of_constr (NamedDecl.get_type d'))) then + if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the body of "++ pr_id id ++ str "."); if check then reorder := check_decl_position env sigma sign d; - d) in + map_named_decl EConstr.Unsafe.to_constr d) in reorder_val_context env sigma sign' !reorder @@ -535,15 +539,16 @@ let prim_refiner r sigma goal = let env = Goal.V82.env sigma goal in let sign = Goal.V82.hyps sigma goal in let cl = Goal.V82.concl sigma goal in - let cl = EConstr.Unsafe.to_constr cl in let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let open EConstr in match r with (* Logical rules *) | Cut (b,replace,id,t) -> (* if !check && not (Retyping.get_sort_of env sigma t) then*) - let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in + let t = EConstr.of_constr t in + let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in let sign,t,cl,sigma = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in @@ -556,14 +561,14 @@ let prim_refiner r sigma goal = user_err ~hdr:"Logic.prim_refiner" (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in - let t = EConstr.of_constr t in let (sg2,ev2,sigma) = - Goal.V82.mk_goal sigma sign (EConstr.of_constr cl) (Goal.V82.extra sigma goal) in - let oterm = EConstr.mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in + Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in + let oterm = mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) | Refine c -> + let cl = EConstr.Unsafe.to_constr cl in check_meta_variables c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in diff --git a/proofs/logic.mli b/proofs/logic.mli index 5fe28ac76..f98248e4d 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -55,7 +55,7 @@ exception RefinerError of refiner_error val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> - Context.Named.Declaration.t -> Environ.named_context_val + EConstr.named_declaration -> Environ.named_context_val val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 9a0b56b84..5c7659ac0 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -22,7 +22,7 @@ let project x = x.sigma (* Getting env *) let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) -let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) +let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) let refiner pr goal_sigma = let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in @@ -198,10 +198,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.Named.t = pf_hyps goal in + let oldhyps = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in - let hyps:Context.Named.t list = + let hyps = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in let newhyps = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 6dcafb77a..56f5facf8 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -10,6 +10,7 @@ open Evd open Proof_type +open EConstr (** The refiner (handles primitive rules and high-level tactics). *) @@ -17,7 +18,7 @@ val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> Context.Named.t +val pf_hyps : goal sigma -> named_context val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 3ed262d6e..4b027a127 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -64,7 +64,7 @@ let pf_get_hyp gls id = raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - id |> pf_get_hyp gls |> NamedDecl.get_type |> EConstr.of_constr + id |> pf_get_hyp gls |> NamedDecl.get_type let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) @@ -199,13 +199,13 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.env gl in let sign = - try Environ.lookup_named id hyps + try EConstr.lookup_named id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign let pf_get_hyp_typ id gl = - pf_get_hyp id gl |> NamedDecl.get_type |> EConstr.of_constr + pf_get_hyp id gl |> NamedDecl.get_type let pf_hyps_types gl = let env = Proofview.Goal.env gl in diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index efc3dbf55..3b23a6ab4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,18 +34,18 @@ val apply_sig_tac : val pf_concl : goal sigma -> types val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> Context.Named.t +val pf_hyps : goal sigma -> named_context (*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> Context.Named.Declaration.t +val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types -val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t +val pf_get_hyp : goal sigma -> Id.t -> named_declaration val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t @@ -117,9 +117,9 @@ module New : sig val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t + val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types diff --git a/tactics/auto.ml b/tactics/auto.ml index 17a488ddb..b548f8b92 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -321,7 +321,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = ( Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let nf c = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) in + let nf c = Evarutil.nf_evar sigma c in let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in let hyp = Context.Named.Declaration.map_constr nf decl in let hintl = make_resolve_hyp env sigma hyp diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ef67d28f9..55fda1c7d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -521,14 +521,14 @@ let evars_to_goals p evm = (** Making local hints *) let make_resolve_hyp env sigma st flags only_classes pri decl = let id = NamedDecl.get_id decl in - let cty = Evarutil.nf_evar sigma (EConstr.of_constr (NamedDecl.get_type decl)) in + let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in let rec iscl env ty = let ctx, ar = decompose_prod_assum sigma ty in match EConstr.kind sigma (fst (decompose_app sigma ar)) with | Const (c,_) -> is_class (ConstRef c) | Ind (i,_) -> is_class (IndRef i) | _ -> - let env' = Environ.push_rel_context ctx env in + let env' = push_rel_context ctx env in let ty' = Reductionops.whd_all env' sigma ar in if not (EConstr.eq_constr sigma ty' ar) then iscl env' ty' else false @@ -562,7 +562,7 @@ let make_hints g st only_classes sign = let consider = try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in (* Section variable, reindex only if the type changed *) - not (Term.eq_constr t (NamedDecl.get_type hyp)) + not (EConstr.eq_constr (project g) (EConstr.of_constr t) (NamedDecl.get_type hyp)) with Not_found -> true in if consider then @@ -617,7 +617,7 @@ module V85 = struct then cached_hints else - let hints = make_hints g st only_classes (Environ.named_context_of_val sign) + let hints = make_hints g st only_classes (EConstr.named_context_of_val sign) in cache := (only_classes, sign, hints); hints @@ -634,7 +634,7 @@ module V85 = struct let gls' = List.map (fun g' -> let env = Goal.V82.env s g' in - let context = Environ.named_context_of_val (Goal.V82.hyps s g') in + let context = EConstr.named_context_of_val (Goal.V82.hyps s g') in let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) (true,false,false) info.only_classes None (List.hd context) in let ldb = Hint_db.add_list env s hint info.hints in @@ -937,9 +937,10 @@ module Search = struct let sign = Goal.hyps g in let (dir, onlyc, sign', cached_hints) = !autogoal_cache in let cwd = Lib.cwd () in + let eq c1 c2 = EConstr.eq_constr (project g) c1 c2 in if DirPath.equal cwd dir && (onlyc == only_classes) && - Context.Named.equal Constr.equal sign sign' && + Context.Named.equal eq sign sign' && Hint_db.transparent_state cached_hints == st then cached_hints else @@ -1033,8 +1034,9 @@ module Search = struct Feedback.msg_debug (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++ pr_ev s' (Proofview.Goal.goal gl')); + let eq c1 c2 = EConstr.eq_constr s' c1 c2 in let hints' = - if b && not (Context.Named.equal Constr.equal (Goal.hyps gl') (Goal.hyps gl)) + if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl)) then let st = Hint_db.transparent_state info.search_hints in make_autogoal_hints info.search_only_classes ~st gl' diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 7173fb4fd..0e28aa980 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -51,7 +51,7 @@ let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 let filter_hyp f tac = let rec seek = function | [] -> Proofview.tclZERO Not_found - | d::rest when f (EConstr.of_constr (NamedDecl.get_type d)) -> tac (NamedDecl.get_id d) + | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in @@ -66,7 +66,7 @@ let contradiction_context = | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | d :: rest -> let id = NamedDecl.get_id d in - let typ = nf_evar sigma (EConstr.of_constr (NamedDecl.get_type d)) in + let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in if is_empty_type sigma typ then simplest_elim (mkVar id) diff --git a/tactics/equality.ml b/tactics/equality.ml index 072da995d..122b64777 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -13,12 +13,12 @@ open Names open Nameops open Term open Termops +open Environ open EConstr open Vars open Namegen open Inductive open Inductiveops -open Environ open Libnames open Globnames open Reductionops @@ -47,10 +47,6 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -let nlocal_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - NamedDecl.LocalAssum (na, inj t) - (* Options *) let discriminate_introduction = ref true @@ -333,7 +329,7 @@ let jmeq_same_dom gl = function | None -> true (* already checked in Hipattern.find_eq_data_decompose *) | Some t -> let rels, t = decompose_prod_assum (project gl) t in - let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in + let env = push_rel_context rels (Proofview.Goal.env gl) in match decompose_app (project gl) t with | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2 | _ -> false @@ -857,16 +853,19 @@ let descend_then env sigma head dirn = let (mib,mip) = lookup_mind_specif env ind in let cstr = get_constructors env indf in let dirn_nlams = cstr.(dirn-1).cs_nargs in - let dirn_env = push_rel_context cstr.(dirn-1).cs_args env in + let dirn_env = Environ.push_rel_context cstr.(dirn-1).cs_args env in (dirn_nlams, dirn_env, (fun dirnval (dfltval,resty) -> let deparsign = make_arity_signature env true indf in + let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in let p = it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in let build_branch i = let result = if Int.equal i dirn then dirnval else dfltval in - it_mkLambda_or_LetIn result (name_context env cstr.(i-1).cs_args) in + let args = name_context env cstr.(i-1).cs_args in + let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) args in + it_mkLambda_or_LetIn result args in let brl = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in @@ -907,11 +906,13 @@ let build_selector env sigma dirn c ind special default = let typ = Retyping.get_type_of env sigma default in let (mib,mip) = lookup_mind_specif env ind in let deparsign = make_arity_signature env true indf in + let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in let p = it_mkLambda_or_LetIn typ deparsign in let cstrs = get_constructors env indf in let build_branch i = let endpt = if Int.equal i dirn then special else default in - it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in + let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstrs.(i-1).cs_args in + it_mkLambda_or_LetIn endpt args in let brl = List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in @@ -995,7 +996,7 @@ let apply_on_clause (f,t) clause = let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let e = next_ident_away eq_baseid (ids_of_context env) in - let e_env = push_named (nlocal_assum (e, t)) env in + let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in let discriminator = build_discriminator e_env sigma dirn (mkVar e) cpath in let sigma,(pf, absurd_term), eff = @@ -1372,7 +1373,7 @@ let simplify_args env sigma t = let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let e = next_ident_away eq_baseid (ids_of_context env) in - let e_env = push_named (nlocal_assum (e,t)) env in + let e_env = push_named (LocalAssum (e,t)) env in let evdref = ref sigma in let filter (cpath, t1', t2') = try @@ -1696,7 +1697,7 @@ let is_eq_x gl x d = | Var id' -> Id.equal id id' | _ -> false in - let c = pf_nf_evar gl (EConstr.of_constr (NamedDecl.get_type d)) in + let c = pf_nf_evar gl (NamedDecl.get_type d) in let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true)); if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false)) @@ -1793,7 +1794,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let find_eq_data_decompose = find_eq_data_decompose gl in let select_equation_name decl = try - let lbeq,u,(_,x,y) = find_eq_data_decompose (EConstr.of_constr (NamedDecl.get_type decl)) in + let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with @@ -1817,7 +1818,6 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in let c = pf_get_hyp hyp gl |> NamedDecl.get_type in - let c = EConstr.of_constr c in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else @@ -1890,7 +1890,7 @@ let rewrite_assumption_cond cond_eq_term cl = let id = NamedDecl.get_id hyp in begin try - let dir = cond_eq_term (EConstr.of_constr (NamedDecl.get_type hyp)) gl in + let dir = cond_eq_term (NamedDecl.get_type hyp) gl in general_rewrite_clause dir false (mkVar id,NoBindings) cl with | Failure _ | UserError _ -> arec rest gl end diff --git a/tactics/hints.ml b/tactics/hints.ml index ef97b0b33..ffd19ac6e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -875,7 +875,7 @@ let make_resolve_hyp env sigma decl = try [make_apply_entry env sigma (true, true, false) None false ~name:(PathHints [VarRef hname]) - (c, EConstr.of_constr (NamedDecl.get_type decl), Univ.ContextSet.empty)] + (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp") @@ -1335,7 +1335,7 @@ let make_local_hint_db env sigma ts eapply lems = (Sigma.to_evar_map sigma, c) in let lems = List.map map lems in - let sign = Environ.named_context env in + let sign = EConstr.named_context env in let ts = match ts with | None -> Hint_db.transparent_state (searchtable_map "core") | Some ts -> ts diff --git a/tactics/hints.mli b/tactics/hints.mli index 344827e03..0d6dd434e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -29,7 +29,7 @@ val decompose_app_bound : evar_map -> constr -> global_reference * constr array type debug = Debug | Info | Off -val secvars_of_hyps : Context.Named.t -> Id.Pred.t +val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t (** Pre-created hint databases *) @@ -209,7 +209,7 @@ val make_resolves : If the hyp cannot be used as a Hint, the empty list is returned. *) val make_resolve_hyp : - env -> evar_map -> Context.Named.Declaration.t -> hint_entry list + env -> evar_map -> named_declaration -> hint_entry list (** [make_extern pri pattern tactic_expr] *) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 607d6d2a9..8e4654c02 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -107,8 +107,8 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = List.for_all (fun decl -> let c = RelDecl.get_type decl in is_local_assum decl && - Term.isRel c && - Int.equal (Term.destRel c) mib.mind_nparams) ctx + isRel sigma c && + Int.equal (destRel sigma c) mib.mind_nparams) ctx then Some (hdapp,args) else None @@ -117,7 +117,6 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) - let cargs = List.map EConstr.of_constr cargs in Some (hdapp,List.rev cargs) else None diff --git a/tactics/inv.ml b/tactics/inv.ml index 426749a75..ecb8eedac 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -13,10 +13,10 @@ open Names open Nameops open Term open Termops +open Environ open EConstr open Vars open Namegen -open Environ open Inductiveops open Printer open Retyping @@ -75,6 +75,7 @@ let make_inv_predicate env evd indf realargs id status concl = | NoDep -> (* We push the arity and leave concl unchanged *) let hyps_arity,_ = get_arity env indf in + let hyps_arity = List.map (fun d -> map_rel_decl EConstr.of_constr d) hyps_arity in (hyps_arity,concl) | Dep dflt_concl -> if not (occur_var env !evd id concl) then @@ -132,6 +133,10 @@ let make_inv_predicate env evd indf realargs id status concl = build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in + let name_context env ctx = + let map f c = List.map (fun d -> Termops.map_rel_decl f d) c in + map EConstr.of_constr (name_context env (map EConstr.Unsafe.to_constr ctx)) + in let predicate = it_mkLambda_or_LetIn newconcl (name_context env hyps) in let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to diff --git a/tactics/leminv.ml b/tactics/leminv.ml index a05b4fbf3..d7c396179 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -12,6 +12,7 @@ open Util open Names open Term open Termops +open Environ open EConstr open Vars open Namegen @@ -20,7 +21,6 @@ open Printer open Reductionops open Entries open Inductiveops -open Environ open Tacmach.New open Clenv open Declare @@ -32,14 +32,6 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -let nlocal_assum (na, t) = - let inj = EConstr.Unsafe.to_constr in - NamedDecl.LocalAssum (na, inj t) - -let nlocal_def (na, b, t) = - let inj = EConstr.Unsafe.to_constr in - NamedDecl.LocalDef (na, inj b, inj t) - let no_inductive_inconstr env sigma constr = (str "Cannot recognize an inductive predicate in " ++ pr_leconstr_env env sigma constr ++ @@ -129,11 +121,11 @@ let rec add_prods_sign env sigma t = | Prod (na,c1,b) -> let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in let b'= subst1 (mkVar id) b in - add_prods_sign (push_named (nlocal_assum (id,c1)) env) sigma b' + add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b' | LetIn (na,c1,t1,b) -> let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in let b'= subst1 (mkVar id) b in - add_prods_sign (push_named (nlocal_def (id,c1,t1)) env) sigma b' + add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b' | _ -> (env,t) (* [dep_option] indicates whether the inversion lemma is dependent or not. @@ -168,6 +160,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let revargs,ownsign = fold_named_context (fun env d (revargs,hyps) -> + let d = map_named_decl EConstr.of_constr d in let id = NamedDecl.get_id d in if Id.List.mem id ivars then ((mkVar id)::revargs, Context.Named.add d hyps) @@ -180,7 +173,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = (pty,goal) in let npty = nf_all env sigma pty in - let extenv = push_named (nlocal_assum (p,npty)) env in + let extenv = push_named (LocalAssum (p,npty)) env in extenv, goal (* [inversion_scheme sign I] @@ -218,6 +211,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let ownSign = ref begin fold_named_context (fun env d sign -> + let d = map_named_decl EConstr.of_constr d in if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign else Context.Named.add d sign) invEnv ~init:Context.Named.empty @@ -231,7 +225,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let h = next_ident_away (Id.of_string "H") !avoid in let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in avoid := h::!avoid; - ownSign := Context.Named.add (nlocal_assum (h,ty)) !ownSign; + ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign; applist (mkVar h, inst) | _ -> EConstr.map sigma fill_holes c in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 9cf3c4187..94f22f903 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -158,7 +158,7 @@ type branch_args = { type branch_assumptions = { ba : branch_args; (* the branch args *) - assums : Context.Named.t} (* the list of assumptions introduced *) + assums : named_context} (* the list of assumptions introduced *) open Misctypes @@ -625,7 +625,6 @@ module New = struct (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - let open EConstr in Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 2b07d937e..e9f623100 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -60,29 +60,29 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic val onNthHypId : int -> (Id.t -> tactic) -> tactic val onNthHyp : int -> (constr -> tactic) -> tactic -val onNthDecl : int -> (Context.Named.Declaration.t -> tactic) -> tactic +val onNthDecl : int -> (named_declaration -> tactic) -> tactic val onLastHypId : (Id.t -> tactic) -> tactic val onLastHyp : (constr -> tactic) -> tactic -val onLastDecl : (Context.Named.Declaration.t -> tactic) -> tactic +val onLastDecl : (named_declaration -> tactic) -> tactic val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic val onNLastHyps : int -> (constr list -> tactic) -> tactic -val onNLastDecls : int -> (Context.Named.t -> tactic) -> tactic +val onNLastDecls : int -> (named_context -> tactic) -> tactic val lastHypId : goal sigma -> Id.t val lastHyp : goal sigma -> constr -val lastDecl : goal sigma -> Context.Named.Declaration.t +val lastDecl : goal sigma -> named_declaration val nLastHypsId : int -> goal sigma -> Id.t list val nLastHyps : int -> goal sigma -> constr list -val nLastDecls : int -> goal sigma -> Context.Named.t +val nLastDecls : int -> goal sigma -> named_context -val afterHyp : Id.t -> goal sigma -> Context.Named.t +val afterHyp : Id.t -> goal sigma -> named_context val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> tactic) -> (Id.t -> tactic) -> Id.t -> tactic -val onHyps : (goal sigma -> Context.Named.t) -> - (Context.Named.t -> tactic) -> tactic +val onHyps : (goal sigma -> named_context) -> + (named_context -> tactic) -> tactic (** {6 Tacticals applying to goal components } *) @@ -110,7 +110,7 @@ type branch_args = private { type branch_assumptions = private { ba : branch_args; (** the branch args *) - assums : Context.Named.t} (** the list of assumptions introduced *) + assums : named_context} (** the list of assumptions introduced *) (** [get_and_check_or_and_pattern loc pats branchsign] returns an appropriate error message if |pats| <> |branchsign|; extends them if no pattern is given @@ -229,7 +229,7 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t + val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> @@ -238,11 +238,11 @@ module New : sig val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic val onLastHypId : (identifier -> unit tactic) -> unit tactic val onLastHyp : (constr -> unit tactic) -> unit tactic - val onLastDecl : (Context.Named.Declaration.t -> unit tactic) -> unit tactic + val onLastDecl : (named_declaration -> unit tactic) -> unit tactic - val onHyps : ([ `NF ], Context.Named.t) Proofview.Goal.enter -> - (Context.Named.t -> unit tactic) -> unit tactic - val afterHyp : Id.t -> (Context.Named.t -> unit tactic) -> unit tactic + val onHyps : ([ `NF ], named_context) Proofview.Goal.enter -> + (named_context -> unit tactic) -> unit tactic + val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic val tryAllHyps : (identifier -> unit tactic) -> unit tactic val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8260c14ad..4bf848a9c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -15,6 +15,7 @@ open Names open Nameops open Term open Termops +open Environ open EConstr open Vars open Find_subterm @@ -22,7 +23,6 @@ open Namegen open Declarations open Inductiveops open Reductionops -open Environ open Globnames open Evd open Pfedit @@ -170,26 +170,6 @@ let _ = (* Primitive tactics *) (******************************************) -let local_assum (na, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - -let nlocal_assum (na, t) = - let open Context.Named.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let nlocal_def (na, b, t) = - let open Context.Named.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) let unsafe_intro env store decl b = @@ -217,8 +197,8 @@ let introduction ?(check=true) id = in let open Context.Named.Declaration in match EConstr.kind sigma concl with - | Prod (_, t, b) -> unsafe_intro env store (nlocal_assum (id, t)) b - | LetIn (_, c, t, b) -> unsafe_intro env store (nlocal_def (id, c, t)) b + | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b + | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b | _ -> raise (RefinerError IntroNeedsProduct) end } @@ -321,7 +301,6 @@ let clear_gen fail = function try clear_hyps_in_evi env evdref (named_context_val env) concl ids with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err in - let concl = EConstr.of_constr concl in let env = reset_with_named_context hyps env in let tac = Refine.refine ~unsafe:true { run = fun sigma -> Evarutil.new_evar env sigma ~principal:true concl @@ -397,18 +376,16 @@ let rename_hyp repl = with Not_found -> () in (** All is well *) - let make_subst (src, dst) = (src, Constr.mkVar dst) in + let make_subst (src, dst) = (src, mkVar dst) in let subst = List.map make_subst repl in - let subst c = CVars.replace_vars subst c in + let subst c = Vars.replace_vars subst c in let map decl = decl |> NamedDecl.map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id) |> NamedDecl.map_constr subst in let nhyps = List.map map hyps in - let concl = EConstr.Unsafe.to_constr concl in let nconcl = subst concl in - let nconcl = EConstr.of_constr nconcl in - let nctx = Environ.val_of_named_context nhyps in + let nctx = val_of_named_context nhyps in let instance = List.map (NamedDecl.get_id %> mkVar) hyps in Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance @@ -435,11 +412,14 @@ let id_of_name_with_default id = function let default_id_of_sort s = if Sorts.is_small s then default_small_ident else default_type_ident +let id_of_name_using_hdchar env c name = + id_of_name_using_hdchar env (EConstr.Unsafe.to_constr c) name + let default_id env sigma decl = let open Context.Rel.Declaration in match decl with | LocalAssum (name,t) -> - let dft = default_id_of_sort (Retyping.get_sort_of env sigma (EConstr.of_constr t)) in + let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in id_of_name_with_default dft name | LocalDef (name,b,_) -> id_of_name_using_hdchar env b name @@ -478,7 +458,7 @@ let find_name mayrepl decl naming gl = match naming with let assert_before_then_gen b naming t tac = let open Context.Rel.Declaration in Proofview.Goal.enter { enter = begin fun gl -> - let id = find_name b (local_assum (Anonymous,t)) naming gl in + let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENLAST (Proofview.V82.tactic (fun gl -> @@ -497,7 +477,7 @@ let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id)) let assert_after_then_gen b naming t tac = let open Context.Rel.Declaration in Proofview.Goal.enter { enter = begin fun gl -> - let id = find_name b (local_assum (Anonymous,t)) naming gl in + let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (fun gl -> @@ -534,7 +514,7 @@ let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast with Not_found -> error "Cannot do a fixpoint on a non inductive type." else let open Context.Rel.Declaration in - check_mutind (push_rel (local_assum (na, c1)) env) sigma (pred k) b + check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b | _ -> error "Not enough products." (* Refine as a fixpoint *) @@ -548,13 +528,14 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl -> let rec mk_sign sign = function | [] -> sign | (f, n, ar) :: oth -> + let open Context.Named.Declaration in let (sp', u') = check_mutind env sigma n ar in if not (eq_mind sp sp') then error "Fixpoints should be on the same mutual inductive declaration."; if mem_named_context_val f sign then user_err ~hdr:"Logic.prim_refiner" (str "Name " ++ pr_id f ++ str " already used in the environment"); - mk_sign (push_named_context_val (nlocal_assum (f, ar)) sign) oth + mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in Refine.refine { run = begin fun sigma -> @@ -584,7 +565,8 @@ let rec check_is_mutcoind env sigma cl = let b = whd_all env sigma cl in match EConstr.kind sigma b with | Prod (na, c1, b) -> - check_is_mutcoind (push_rel (local_assum (na,c1)) env) sigma b + let open Context.Rel.Declaration in + check_is_mutcoind (push_rel (LocalAssum (na,c1)) env) sigma b | _ -> try let _ = find_coinductive env sigma b in () @@ -602,9 +584,10 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl -> let rec mk_sign sign = function | [] -> sign | (f, ar) :: oth -> + let open Context.Named.Declaration in if mem_named_context_val f sign then error "Name already used in the environment."; - mk_sign (push_named_context_val (nlocal_assum (f, ar)) sign) oth + mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in Refine.refine { run = begin fun sigma -> @@ -640,16 +623,13 @@ let pf_reduce_decl redfun where decl gl = let redfun' c = Tacmach.New.pf_apply redfun gl c in match decl with | LocalAssum (id,ty) -> - let ty = EConstr.of_constr ty in if where == InHypValueOnly then user_err (pr_id id ++ str " has no value."); - nlocal_assum (id,redfun' ty) + LocalAssum (id,redfun' ty) | LocalDef (id,b,ty) -> - let b = EConstr.of_constr b in - let ty = EConstr.of_constr ty in let b' = if where != InHypTypeOnly then redfun' b else b in let ty' = if where != InHypValueOnly then redfun' ty else ty in - nlocal_def (id,b',ty') + LocalDef (id,b',ty') (* Possibly equip a reduction with the occurrences mentioned in an occurrence clause *) @@ -744,17 +724,14 @@ let pf_e_reduce_decl redfun where decl gl = let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma c in match decl with | LocalAssum (id,ty) -> - let ty = EConstr.of_constr ty in if where == InHypValueOnly then user_err (pr_id id ++ str " has no value."); let Sigma (ty', sigma, p) = redfun sigma ty in - Sigma (nlocal_assum (id, ty'), sigma, p) + Sigma (LocalAssum (id, ty'), sigma, p) | LocalDef (id,b,ty) -> - let b = EConstr.of_constr b in - let ty = EConstr.of_constr ty in let Sigma (b', sigma, p) = if where != InHypTypeOnly then redfun sigma b else Sigma.here b sigma in let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in - Sigma (nlocal_def (id, b', ty'), sigma, p +> q) + Sigma (LocalDef (id, b', ty'), sigma, p +> q) let e_reduct_in_concl ~check (redfun, sty) = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> @@ -787,21 +764,18 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm let open Context.Named.Declaration in match decl with | LocalAssum (id,ty) -> - let ty = EConstr.of_constr ty in if where == InHypValueOnly then user_err (pr_id id ++ str " has no value."); let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in - Sigma (nlocal_assum (id, ty'), sigma, p) + Sigma (LocalAssum (id, ty'), sigma, p) | LocalDef (id,b,ty) -> - let b = EConstr.of_constr b in - let ty = EConstr.of_constr ty in let Sigma (b', sigma, p) = if where != InHypTypeOnly then (redfun true).e_redfun env sigma b else Sigma.here b sigma in let Sigma (ty', sigma, q) = if where != InHypValueOnly then (redfun false).e_redfun env sigma ty else Sigma.here ty sigma in - Sigma (nlocal_def (id,b',ty'), sigma, p +> q) + Sigma (LocalDef (id,b',ty'), sigma, p +> q) let e_change_in_hyp redfun (id,where) = Proofview.Goal.s_enter { s_enter = begin fun gl -> @@ -974,10 +948,10 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in match EConstr.kind sigma concl with | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) -> - let name = find_name false (local_assum (name,t)) name_flag gl in + let name = find_name false (LocalAssum (name,t)) name_flag gl in build_intro_tac name move_flag tac | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> - let name = find_name false (local_def (name,b,t)) name_flag gl in + let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac | _ -> begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct) @@ -1382,11 +1356,11 @@ let enforce_prop_bound_names rename tac = Name (add_suffix Namegen.default_prop_ident s) else na in - mkProd (na,t,aux (push_rel (local_assum (na,t)) env) sigma (i-1) t') + mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t') | Prod (Anonymous,t,t') -> - mkProd (Anonymous,t,aux (push_rel (local_assum (Anonymous,t)) env) sigma (i-1) t') + mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t') | LetIn (na,c,t,t') -> - mkLetIn (na,c,t,aux (push_rel (local_def (na,c,t)) env) sigma (i-1) t') + mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t') | _ -> assert false in let rename_branch i = Proofview.Goal.nf_enter { enter = begin fun gl -> @@ -1619,11 +1593,11 @@ let make_projection env sigma params cstr sign elim i n c u = let elim = match elim with | NotADefinedRecordUseScheme elim -> (* bugs: goes from right to left when i increases! *) - let decl = List.nth cstr.cs_args i in + let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.cs_args in + let decl = List.nth cs_args i in let t = RelDecl.get_type decl in - let t = EConstr.of_constr t in - let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> EConstr.of_constr b in - let branch = it_mkLambda_or_LetIn b cstr.cs_args in + let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in + let branch = it_mkLambda_or_LetIn b cs_args in if (* excludes dependent projection types *) noccur_between sigma 1 (n-i-1) t @@ -1890,7 +1864,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming if with_delta then default_unify_flags () else default_no_delta_unify_flags () in let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in - let targetid = find_name true (local_assum (Anonymous,t')) naming gl in + let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in let rec aux idstoclear with_destruct c = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in @@ -2017,7 +1991,6 @@ let assumption = else Tacticals.New.tclZEROMSG (str "No such assumption.") | decl::rest -> let t = NamedDecl.get_type decl in - let t = EConstr.of_constr t in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let (sigma, is_same_type) = @@ -2058,13 +2031,13 @@ let check_is_type env sigma ty = let check_decl env sigma decl = let open Context.Named.Declaration in - let ty = EConstr.of_constr (NamedDecl.get_type decl) in + let ty = NamedDecl.get_type decl in let evdref = ref sigma in try let _ = Typing.e_sort_of env evdref ty in let _ = match decl with | LocalAssum _ -> () - | LocalDef (_,c,_) -> Typing.e_check env evdref (EConstr.of_constr c) ty + | LocalDef (_,c,_) -> Typing.e_check env evdref c ty in !evdref with e when CErrors.noncritical e -> @@ -2146,6 +2119,7 @@ let keep hyps = let sigma = Tacmach.New.project gl in let cl,_ = fold_named_context_reverse (fun (clear,keep) decl -> + let decl = map_named_decl EConstr.of_constr decl in let hyp = NamedDecl.get_id decl in if Id.List.mem hyp hyps || List.exists (occur_var_in_decl env sigma hyp) keep @@ -2692,6 +2666,7 @@ let insert_before decls lasthyp env = | Some id -> Environ.fold_named_context (fun _ d env -> + let d = map_named_decl EConstr.of_constr d in let env = if Id.equal id (NamedDecl.get_id d) then push_named_context decls env else env in push_named d env) ~init:(reset_context env) env @@ -2701,8 +2676,8 @@ let insert_before decls lasthyp env = let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let open Context.Named.Declaration in let t = match ty with Some t -> t | _ -> typ_of env sigma c in - let decl = if dep then nlocal_def (id,c,t) - else nlocal_assum (id,t) + let decl = if dep then LocalDef (id,c,t) + else LocalAssum (id,t) in match with_eq with | Some (lr,(loc,ido)) -> @@ -2721,7 +2696,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let refl = EConstr.of_constr refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in - let newenv = insert_before [nlocal_assum (heq,eq); decl] lastlhyp env in + let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store ccl in Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r) | None -> @@ -2822,8 +2797,8 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in let na = generalized_name sigma c t ids cl' na in let decl = match b with - | None -> local_assum (na,t) - | Some b -> local_def (na,b,t) + | None -> LocalAssum (na,t) + | Some b -> LocalDef (na,b,t) in mkProd_or_LetIn decl cl', sigma' @@ -2838,7 +2813,7 @@ let old_generalize_dep ?(with_let=false) c gl = let sign = pf_hyps gl in let sigma = project gl in let init_ids = ids_of_named_context (Global.named_context()) in - let seek (d:Context.Named.Declaration.t) (toquant:Context.Named.t) = + let seek (d:named_declaration) (toquant:named_context) = if List.exists (fun d' -> occur_var_in_decl env sigma (NamedDecl.get_id d') d) toquant || dependent_in_decl sigma c d then d::toquant @@ -2862,7 +2837,6 @@ let old_generalize_dep ?(with_let=false) c gl = | _ -> None else None in - let body = Option.map EConstr.of_constr body in let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) (cl',project gl) in (** Check that the generalization is indeed well-typed *) @@ -3256,7 +3230,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = | Var id -> id | _ -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar (Global.env()) (EConstr.Unsafe.to_constr (type_of c)) Anonymous in + id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) @@ -3342,6 +3316,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = let before = ref true in let maindep = ref false in let seek_deps env decl rhyp = + let decl = map_named_decl EConstr.of_constr decl in let hyp = NamedDecl.get_id decl in if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then begin @@ -3434,15 +3409,15 @@ type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - params: Context.Rel.t; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (* number of parameters *) - predicates: Context.Rel.t; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) npredicates: int; (* Number of predicates *) - branches: Context.Rel.t; (* branchr,...,branch1 *) + branches: rel_context; (* branchr,...,branch1 *) nbranches: int; (* Number of branches *) - args: Context.Rel.t; (* (xni, Ti_ni) ... (x1, Ti_1) *) + args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *) nargs: int; (* number of arguments *) - indarg: Context.Rel.Declaration.t option; (* Some (H,I prm1..prmp x1...xni) + indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise *) concl: types; (* Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive *) @@ -3586,10 +3561,10 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = in (* Abstract by equalities *) let eqs = lift_togethern 1 eqs in (* lift together and past genarg *) - let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> local_assum (Anonymous, x)) eqs) in + let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> LocalAssum (Anonymous, x)) eqs) in let decl = match body with - | None -> local_assum (Name id, c) - | Some body -> local_def (Name id, body, c) + | None -> LocalAssum (Name id, c) + | Some body -> LocalDef (Name id, body, c) in (* Abstract by the "generalized" hypothesis. *) let genarg = mkProd_or_LetIn decl abseqs in @@ -3668,7 +3643,6 @@ let abstract_args gl generalize_vars dep id defined f args = let decl = List.hd rel in RelDecl.get_name decl, RelDecl.get_type decl, c in - let ty = EConstr.of_constr ty in let argty = Tacmach.pf_unsafe_type_of gl arg in let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in let () = sigma := sigma' in @@ -3681,7 +3655,7 @@ let abstract_args gl generalize_vars dep id defined f args = Id.Set.add id nongenvars, Id.Set.remove id vars, env) | _ -> let name = get_id name in - let decl = local_assum (Name name, ty) in + let decl = LocalAssum (Name name, ty) in let ctx = decl :: ctx in let c' = mkApp (lift 1 c, [|mkRel 1|]) in let args = arg :: args in @@ -3739,10 +3713,9 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = let (f, args, def, id, oldid) = let oldid = Tacmach.New.pf_get_new_id id gl in match Tacmach.New.pf_get_hyp id gl with - | LocalAssum (_,t) -> let f, args = decompose_app sigma (EConstr.of_constr t) in + | LocalAssum (_,t) -> let f, args = decompose_app sigma t in (f, args, false, id, oldid) | LocalDef (_,t,_) -> - let t = EConstr.of_constr t in let f, args = decompose_app sigma t in (f, args, true, id, oldid) in @@ -3809,13 +3782,13 @@ let specialize_eqs id gl = if in_eqs then acc, in_eqs, ctx, ty else let e = e_new_evar (push_rel_context ctx env) evars t in - aux false (local_def (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) + aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) | t -> acc, in_eqs, ctx, ty in let acc, worked, ctx, ty = aux false [] (mkVar id) ty in let ctx' = nf_rel_context_evar !evars ctx in let ctx'' = List.map (function - | LocalDef (n,k,t) when isEvar !evars (EConstr.of_constr k) -> LocalAssum (n,t) + | LocalDef (n,k,t) when isEvar !evars k -> LocalAssum (n,t) | decl -> decl) ctx' in let ty' = it_mkProd_or_LetIn ty ctx'' in @@ -3855,13 +3828,13 @@ let decompose_paramspred_branch_args sigma elimt = | Prod(nme,tpe,elimt') -> let hd_tpe,_ = decompose_app sigma (snd (decompose_prod_assum sigma tpe)) in if not (occur_rel sigma 1 elimt') && isRel sigma hd_tpe - then cut_noccur elimt' (local_assum (nme,tpe)::acc2) + then cut_noccur elimt' (LocalAssum (nme,tpe)::acc2) else let acc3,ccl = decompose_prod_assum sigma elimt in acc2 , acc3 , ccl | App(_, _) | Rel _ -> acc2 , [] , elimt | _ -> error_ind_scheme "" in let rec cut_occur elimt acc1 = match EConstr.kind sigma elimt with - | Prod(nme,tpe,c) when occur_rel sigma 1 c -> cut_occur c (local_assum (nme,tpe)::acc1) + | Prod(nme,tpe,c) when occur_rel sigma 1 c -> cut_occur c (LocalAssum (nme,tpe)::acc1) | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl | App(_, _) | Rel _ -> acc1,[],[],elimt | _ -> error_ind_scheme "" in @@ -3939,7 +3912,6 @@ let compute_elim_sig sigma ?elimc elimt = match List.hd args_indargs with | LocalDef (hiname,_,hi) -> error_ind_scheme "" | LocalAssum (hiname,hi) -> - let hi = EConstr.of_constr hi in let hi_ind, hi_args = decompose_app sigma hi in let hi_is_ind = (* hi est d'un type globalisable *) match EConstr.kind sigma hi_ind with @@ -3965,7 +3937,6 @@ let compute_elim_sig sigma ?elimc elimt = | None -> !res (* No indref *) | Some (LocalDef _) -> error_ind_scheme "" | Some (LocalAssum (_,ind)) -> - let ind = EConstr.of_constr ind in let indhd,indargs = decompose_app sigma ind in try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) } with e when CErrors.noncritical e -> @@ -3983,7 +3954,6 @@ let compute_scheme_signature evd scheme names_info ind_type_guess = let cond hd = EConstr.eq_constr evd hd ind_type_guess && not scheme.farg_in_concl in (cond, fun _ _ -> ()) | Some (LocalAssum (_,ind)) -> (* Standard scheme from an inductive type *) - let ind = EConstr.of_constr ind in let indhd,indargs = decompose_app evd ind in let cond hd = EConstr.eq_constr evd hd indhd in let check_concl is_pred p = @@ -4016,7 +3986,6 @@ let compute_scheme_signature evd scheme names_info ind_type_guess = let rec find_branches p lbrch = match lbrch with | LocalAssum (_,t) :: brs -> - let t = EConstr.of_constr t in (try let lchck_brch = check_branch p t in let n = List.fold_left @@ -4123,7 +4092,7 @@ let get_eliminator elim dep s gl = | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in - let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (EConstr.of_constr (RelDecl.get_type d)))) + let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d))) (List.rev s.branches) in evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l @@ -4465,7 +4434,6 @@ let induction_gen clear_flag isrec with_evars elim declaring the induction argument as a new local variable *) let id = (* Type not the right one if partially applied but anyway for internal use*) - let t = EConstr.Unsafe.to_constr t in let x = id_of_name_using_hdchar (Global.env()) t Anonymous in new_fresh_id [] x gl in let info_arg = (is_arg_pure_hyp, not enough_applied) in @@ -4503,7 +4471,7 @@ let induction_gen_l isrec with_evars elim names lc = let type_of = Tacmach.New.pf_unsafe_type_of gl in let sigma = Tacmach.New.project gl in let x = - id_of_name_using_hdchar (Global.env()) (EConstr.Unsafe.to_constr (type_of c)) Anonymous in + 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 -> replace_term sigma c (mkVar id) r) l' in @@ -4863,6 +4831,9 @@ let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n) (** d1 is the section variable in the global context, d2 in the goal context *) let interpretable_as_section_decl evd d1 d2 = let open Context.Named.Declaration in + let e_eq_constr_univs sigma c1 c2 = + e_eq_constr_univs sigma (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) + in match d2, d1 with | LocalDef _, LocalAssum _ -> false | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b0d9dcb1c..0087d607d 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -35,9 +35,9 @@ val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool val introduction : ?check:bool -> Id.t -> unit Proofview.tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic -val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic +val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic -val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic +val convert_hyp_no_check : named_declaration -> unit Proofview.tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic val fix : Id.t option -> int -> unit Proofview.tactic @@ -51,7 +51,7 @@ val convert_leq : constr -> constr -> unit Proofview.tactic val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t -val find_intro_names : Context.Rel.t -> goal sigma -> Id.t list +val find_intro_names : rel_context -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic @@ -185,7 +185,7 @@ val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) val apply_type : constr -> constr list -> unit Proofview.tactic -val bring_hyps : Context.Named.t -> unit Proofview.tactic +val bring_hyps : named_context -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic @@ -244,15 +244,15 @@ type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - params: Context.Rel.t; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (** number of parameters *) - predicates: Context.Rel.t; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) npredicates: int; (** Number of predicates *) - branches: Context.Rel.t; (** branchr,...,branch1 *) + branches: rel_context; (** branchr,...,branch1 *) nbranches: int; (** Number of branches *) - args: Context.Rel.t; (** (xni, Ti_ni) ... (x1, Ti_1) *) + args: rel_context; (** (xni, Ti_ni) ... (x1, Ti_1) *) nargs: int; (** number of arguments *) - indarg: Context.Rel.Declaration.t option; (** Some (H,I prm1..prmp x1...xni) + indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise *) concl: types; (** Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive *) diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 219abb7fd..2c863c42a 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -344,7 +344,7 @@ struct ) (pr_dconstr pr_term_pattern) p*) let search_pat cpat dpat dn = - let whole_c = cpat in + let whole_c = EConstr.of_constr cpat in (* if we are at the root, add an empty context *) let dpat = under_prod (empty_ctx dpat) in TDnet.Idset.fold @@ -352,9 +352,8 @@ struct 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) c_id (** FIXME *) + try Termops.align_prod_letin Evd.empty 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/classes.ml b/toplevel/classes.ml index 7a5d0ed81..165663ef6 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -150,6 +150,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p in let k, u, cty, ctx', ctx, len, imps, subst = let impls, ((env', ctx), imps) = interp_context_evars env evars ctx in + let ctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) ctx in let c', imps' = interp_type_evars_impls ~impls env' evars tclass in let c' = EConstr.Unsafe.to_constr c' in let len = List.length ctx in @@ -363,6 +364,7 @@ let context poly l = let env = Global.env() in let evars = ref (Evd.from_env env) in let _, ((env', fullctx), impls) = interp_context_evars env evars l in + let fullctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) fullctx in let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in let fullctx = Context.Rel.map subst fullctx in let ce t = Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr t) in diff --git a/toplevel/command.ml b/toplevel/command.ml index 44fc4eb1a..b1415515f 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -95,6 +95,7 @@ let interp_definition pl bl p red_option c ctypopt = let ctx = Evd.make_evar_universe_context env pl in let evdref = ref (Evd.from_ctx ctx) in let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in + let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in let nb_args = List.length ctx in let imps,pl,ce = match ctypopt with @@ -581,6 +582,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let _, ((env_params, ctx_params), userimpls) = interp_context_evars env0 evdref paramsl in + let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in let indnames = List.map (fun ind -> ind.ind_name) indl in (* Names of parameters as arguments of the inductive type (defs removed) *) @@ -850,16 +852,16 @@ let interp_fix_context env evdref isfix fix = let interp_fix_ccl evdref impls (env,_) fix = let (c, impl) = interp_type_evars_impls ~impls env evdref fix.fix_type in - (EConstr.Unsafe.to_constr c, impl) + (c, impl) let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = + let open EConstr in Option.map (fun body -> let env = push_rel_context ctx env_rec in let body = interp_casted_constr_evars env evdref ~impls body ccl in - let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body ctx) fix.fix_body -let build_fix_type (_,ctx) ccl = Term.it_mkProd_or_LetIn ccl ctx +let build_fix_type (_,ctx) ccl = EConstr.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 @@ -899,7 +901,7 @@ let fixsub_module = subtac_dir @ ["Wf"] let tactics_module = subtac_dir @ ["Tactics"] let init_reference dir s () = Coqlib.gen_reference "Command" dir s -let init_constant dir s () = Coqlib.gen_constant "Command" dir s +let init_constant dir s () = EConstr.of_constr (Coqlib.gen_constant "Command" dir s) let make_ref l s = init_reference l s let fix_proto = init_constant tactics_module "fix_proto" let fix_sub_ref = make_ref fixsub_module "Fix_sub" @@ -907,14 +909,17 @@ let measure_on_R_ref = make_ref fixsub_module "MR" let well_founded = init_constant ["Init"; "Wf"] "well_founded" let mkSubset name typ prop = let open EConstr in - EConstr.Unsafe.to_constr (mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ), - [| typ; mkLambda (name, typ, prop) |])) + mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ), + [| typ; mkLambda (name, typ, prop) |]) let sigT = Lazy.from_fun build_sigma_type let make_qref s = Qualid (Loc.ghost, qualid_of_string s) let lt_ref = make_qref "Init.Peano.lt" -let rec telescope = function +let rec telescope l = + let open EConstr in + let open Vars in + match l with | [] -> assert false | [LocalAssum (n, t)] -> t, [LocalDef (n, mkRel 1, t)], mkRel 1 | LocalAssum (n, t) :: tl -> @@ -924,7 +929,9 @@ let rec telescope = function let t = RelDecl.get_type decl in let pred = mkLambda (RelDecl.get_name decl, t, ty) in let ty = Universes.constr_of_global (Lazy.force sigT).typ in + let ty = EConstr.of_constr ty in let intro = Universes.constr_of_global (Lazy.force sigT).intro in + let intro = EConstr.of_constr intro in let sigty = mkApp (ty, [|t; pred|]) in let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in (sigty, pred :: tys, (succ k, intro))) @@ -934,9 +941,11 @@ let rec telescope = function (fun pred decl (prev, subst) -> let t = RelDecl.get_type decl in let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in + let p1 = EConstr.of_constr p1 in let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in - let proj1 = applistc p1 [t; pred; prev] in - let proj2 = applistc p2 [t; pred; prev] in + let p2 = EConstr.of_constr p2 in + let proj1 = applist (p1, [t; pred; prev]) in + let proj2 = applist (p2, [t; pred; prev]) in (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) (List.rev tys) tl (mkRel 1, []) in ty, (LocalDef (n, last, t) :: subst), constr @@ -945,11 +954,12 @@ let rec telescope = function ty, (LocalDef (n, b, t) :: subst), lift 1 term let nf_evar_context sigma ctx = - List.map (map_constr (fun c -> EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)))) ctx + List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let open EConstr in let open Vars in + let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in let ctx = Evd.make_evar_universe_context env pl in @@ -960,10 +970,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let top_arity = interp_type_evars top_env evdref arityc in let full_arity = it_mkProd_or_LetIn top_arity binders_rel in let argtyp, letbinders, make = telescope binders_rel in - let make = EConstr.of_constr make in let argname = Id.of_string "recarg" in let arg = LocalAssum (Name argname, argtyp) in - let argtyp = EConstr.of_constr argtyp in let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in @@ -978,10 +986,11 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in match ctx, EConstr.kind !evdref ar with | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null) - when Reductionops.is_conv env !evdref (EConstr.of_constr t) (EConstr.of_constr u) -> t + when Reductionops.is_conv env !evdref t u -> t | _, _ -> error () with e when CErrors.noncritical e -> error () in + let relargty = EConstr.Unsafe.to_constr relargty in let measure = interp_casted_constr_evars binders_env evdref measure relargty in let wf_rel, wf_rel_fun, measure_fn = let measure_body, measure = @@ -996,7 +1005,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = subst1 y measure_body |]) in wf_rel, wf_rel_fun, measure in - let wf_proof = mkApp (EConstr.of_constr (delayed_force well_founded), [| argtyp ; wf_rel |]) in + let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in let argid' = Id.of_string (Id.to_string argname ^ "'") in let wfarg len = LocalAssum (Name argid', mkSubset (Name argid') argtyp @@ -1014,7 +1023,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = (* 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 = EConstr.Unsafe.to_constr intern_fun_arity_prod 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 @@ -1022,16 +1030,13 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in let rcurry = mkApp (rel, [| measure; lift len measure |]) in - let rcurry = EConstr.Unsafe.to_constr rcurry 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 body = EConstr.Unsafe.to_constr body in - let ty = EConstr.Unsafe.to_constr ty in LocalDef (Name recname, body, ty) in let fun_bl = intern_fun_binder :: [arg] in - let lift_lets = Termops.lift_rel_context 1 letbinders in + let lift_lets = lift_rel_context 1 letbinders in let intern_body = let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in let (r, l, impls, scopes) = @@ -1099,6 +1104,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let interp_recursive isfix fixl notations = let open Context.Named.Declaration in + let open EConstr in let env = Global.env() in let fixnames = List.map (fun fix -> fix.fix_name) fixl in @@ -1119,20 +1125,19 @@ let interp_recursive isfix fixl notations = let fixctximpenvs, fixctximps = List.split fiximppairs in let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in let fixtypes = List.map2 build_fix_type fixctxs fixccls in - let fixtypes = List.map (fun c -> EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.of_constr c))) fixtypes in + let fixtypes = List.map (fun c -> nf_evar !evdref c) fixtypes in let fiximps = List.map3 (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps)) fixctximps fixcclimps fixctxs in let rec_sign = List.fold_left2 (fun env' id t -> - if Flags.is_program_mode () then - let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref (EConstr.of_constr t) in - let sort = EConstr.Unsafe.to_constr sort in + if Flags.is_program_mode () then + let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in - EConstr.Unsafe.to_constr (Typing.e_solve_evars env evdref (EConstr.of_constr app)) + Typing.e_solve_evars env evdref app with e when CErrors.noncritical e -> t in LocalAssum (id,fixprot) :: env' @@ -1142,6 +1147,8 @@ let interp_recursive isfix fixl notations = let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) + let fixtypes = List.map EConstr.Unsafe.to_constr fixtypes in + let fixccls = List.map EConstr.Unsafe.to_constr fixccls in let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in (* Interp bodies with rollback because temp use of notations/implicit *) @@ -1156,6 +1163,7 @@ let interp_recursive isfix fixl notations = (* Instantiate evars and check all are resolved *) let evd = consider_remaining_unif_problems env_rec !evdref in let evd, nf = nf_evars_and_universes evd in + let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 851b87903..b689dfcf9 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -29,56 +29,56 @@ module RelDecl = Context.Rel.Declaration (* This simplifies the typing context of Cases clauses *) (* hope it does not disturb other typing contexts *) -let contract env lc = +let contract env sigma lc = + let open EConstr in let l = ref [] in let contract_context decl env = match decl with - | LocalDef (_,c',_) when isRel c' -> + | LocalDef (_,c',_) when isRel sigma c' -> l := (Vars.substl !l c') :: !l; env | _ -> let t = Vars.substl !l (RelDecl.get_type decl) in - let decl = decl |> RelDecl.map_name (named_hd env t) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in + let decl = decl |> RelDecl.map_name (named_hd env (EConstr.Unsafe.to_constr t)) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in l := (mkRel 1) :: List.map (Vars.lift 1) !l; push_rel decl env in let env = process_rel_context contract_context env in (env, List.map (Vars.substl !l) lc) -let contract2 env a b = match contract env [a;b] with +let contract2 env sigma a b = match contract env sigma [a;b] with | env, [a;b] -> env,a,b | _ -> assert false -let contract3 env a b c = match contract env [a;b;c] with +let contract3 env sigma a b c = match contract env sigma [a;b;c] with | env, [a;b;c] -> env,a,b,c | _ -> assert false -let contract4 env a b c d = match contract env [a;b;c;d] with +let contract4 env sigma a b c d = match contract env sigma [a;b;c;d] with | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false -let contract1_vect env a v = - match contract env (a :: Array.to_list v) with +let contract1_vect env sigma a v = + match contract env sigma (a :: Array.to_list v) with | env, a::l -> env,a,Array.of_list l | _ -> assert false -let rec contract3' env a b c = function +let rec contract3' env sigma a b c = function | OccurCheck (evk,d) -> - let d = EConstr.Unsafe.to_constr d in - let x,d = contract4 env a b c d in x,OccurCheck(evk, EConstr.of_constr d) + let x,d = contract4 env sigma a b c d in x,OccurCheck(evk, d) | NotClean ((evk,args),env',d) -> - let d = EConstr.Unsafe.to_constr d in - let args = Array.map EConstr.Unsafe.to_constr args in - let env',d,args = contract1_vect env' d args in - contract3 env a b c,NotClean((evk,Array.map EConstr.of_constr args),env',EConstr.of_constr d) + let env',d,args = contract1_vect env' sigma d args in + contract3 env sigma a b c,NotClean((evk,args),env',d) | ConversionFailed (env',t1,t2) -> - let t1 = EConstr.Unsafe.to_constr t1 in - let t2 = EConstr.Unsafe.to_constr t2 in - let (env',t1,t2) = contract2 env' t1 t2 in - contract3 env a b c, ConversionFailed (env',EConstr.of_constr t1,EConstr.of_constr t2) + let (env',t1,t2) = contract2 env' sigma t1 t2 in + contract3 env sigma a b c, ConversionFailed (env',t1,t2) | NotSameArgSize | NotSameHead | NoCanonicalStructure | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities - | UnifUnivInconsistency _ as x -> contract3 env a b c, x + | UnifUnivInconsistency _ as x -> contract3 env sigma a b c, x | CannotSolveConstraint ((pb,env',t,u),x) -> - let env',t,u = contract2 env' t u in - let y,x = contract3' env a b c x in + let t = EConstr.of_constr t in + let u = EConstr.of_constr u in + let env',t,u = contract2 env' sigma t u in + let t = EConstr.Unsafe.to_constr t in + let u = EConstr.Unsafe.to_constr u in + let y,x = contract3' env sigma a b c x in y,CannotSolveConstraint ((pb,env',t,u),x) (** Ad-hoc reductions *) @@ -820,29 +820,19 @@ let explain_pretype_error env sigma err = match err with | CantFindCaseType c -> explain_cant_find_case_type env sigma c | ActualTypeNotCoercible (j,t,e) -> - let j = to_unsafe_judgment j in - let t = EConstr.Unsafe.to_constr t in let {uj_val = c; uj_type = actty} = j in - let (env, c, actty, expty), e = contract3' env c actty t e in + let (env, c, actty, expty), e = contract3' env sigma c actty t e in let j = {uj_val = c; uj_type = actty} in - explain_actual_type env sigma (on_judgment EConstr.of_constr j) (EConstr.of_constr expty) (Some e) + explain_actual_type env sigma j expty (Some e) | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp | VarNotFound id -> explain_var_not_found env id | UnexpectedType (actual,expect) -> - let actual = EConstr.Unsafe.to_constr actual in - let expect = EConstr.Unsafe.to_constr expect in - let env, actual, expect = contract2 env actual expect in - let actual = EConstr.of_constr actual in - let expect = EConstr.of_constr expect in + let env, actual, expect = contract2 env sigma actual expect in explain_unexpected_type env sigma actual expect | NotProduct c -> explain_not_product env sigma c | CannotUnify (m,n,e) -> - let m = EConstr.Unsafe.to_constr m in - let n = EConstr.Unsafe.to_constr n in - let env, m, n = contract2 env m n in - let m = EConstr.of_constr m in - let n = EConstr.of_constr n in + let env, m, n = contract2 env sigma m n in explain_cannot_unify env sigma m n e | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn | CannotGeneralize ty -> explain_refiner_cannot_generalize env sigma ty diff --git a/toplevel/record.ml b/toplevel/record.ml index ec719bca8..af2377e51 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -114,6 +114,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = | LocalPattern _ -> assert false) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in + let newps = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) newps in let t', template = match t with | Some t -> let env = push_rel_context newps env0 in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cf3da7e02..f3d73b76c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1651,7 +1651,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = let natureofid = match decl with | LocalAssum _ -> "Hypothesis" | LocalDef (_,bdy,_) ->"Constant (let in)" in - v 0 (pr_id id ++ str":" ++ pr_constr (NamedDecl.get_type decl) ++ fnl() ++ fnl() + v 0 (pr_id id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl() ++ str natureofid ++ str " of the goal context.") with (* fallback to globals *) | NoHyp | Not_found -> print_about ref_or_by_not |