aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-26 16:18:47 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:30:44 +0100
commitb4b90c5d2e8c413e1981c456c933f35679386f09 (patch)
treefc84ec244390beb2f495b024620af2e130ad5852
parent78a8d59b39dfcb07b94721fdcfd9241d404905d2 (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.
-rw-r--r--engine/eConstr.ml105
-rw-r--r--engine/eConstr.mli48
-rw-r--r--engine/evarutil.ml18
-rw-r--r--engine/evarutil.mli99
-rw-r--r--engine/proofview.ml2
-rw-r--r--engine/proofview.mli15
-rw-r--r--engine/termops.ml94
-rw-r--r--engine/termops.mli49
-rw-r--r--interp/constrintern.ml4
-rw-r--r--interp/constrintern.mli4
-rw-r--r--ltac/rewrite.ml43
-rw-r--r--ltac/rewrite.mli4
-rw-r--r--ltac/tactic_matching.ml4
-rw-r--r--ltac/tactic_matching.mli2
-rw-r--r--plugins/cc/cctac.ml8
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml15
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/firstorder/instances.ml3
-rw-r--r--plugins/firstorder/rules.ml2
-rw-r--r--plugins/fourier/fourierR.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml7
-rw-r--r--plugins/funind/functional_principles_types.ml16
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/invfun.ml20
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/omega/coq_omega.ml30
-rw-r--r--plugins/rtauto/refl_tauto.ml28
-rw-r--r--plugins/rtauto/refl_tauto.mli6
-rw-r--r--plugins/ssrmatching/ssrmatching.ml44
-rw-r--r--pretyping/cases.ml100
-rw-r--r--pretyping/cases.mli8
-rw-r--r--pretyping/coercion.ml14
-rw-r--r--pretyping/constr_matching.ml26
-rw-r--r--pretyping/evarconv.ml16
-rw-r--r--pretyping/evardefine.ml15
-rw-r--r--pretyping/evarsolve.ml27
-rw-r--r--pretyping/find_subterm.ml4
-rw-r--r--pretyping/find_subterm.mli4
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/patternops.ml17
-rw-r--r--pretyping/pretyping.ml52
-rw-r--r--pretyping/reductionops.ml40
-rw-r--r--pretyping/reductionops.mli6
-rw-r--r--pretyping/retyping.ml24
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/tacred.ml55
-rw-r--r--pretyping/typeclasses.ml1
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--pretyping/typing.ml21
-rw-r--r--pretyping/unification.ml8
-rw-r--r--pretyping/unification.mli2
-rw-r--r--printing/prettyp.ml8
-rw-r--r--proofs/goal.ml1
-rw-r--r--proofs/logic.ml21
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/refiner.ml6
-rw-r--r--proofs/refiner.mli3
-rw-r--r--proofs/tacmach.ml6
-rw-r--r--proofs/tacmach.mli10
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/class_tactics.ml16
-rw-r--r--tactics/contradiction.ml4
-rw-r--r--tactics/equality.ml30
-rw-r--r--tactics/hints.ml4
-rw-r--r--tactics/hints.mli4
-rw-r--r--tactics/hipattern.ml5
-rw-r--r--tactics/inv.ml7
-rw-r--r--tactics/leminv.ml20
-rw-r--r--tactics/tacticals.ml3
-rw-r--r--tactics/tacticals.mli28
-rw-r--r--tactics/tactics.ml161
-rw-r--r--tactics/tactics.mli18
-rw-r--r--tactics/term_dnet.ml5
-rw-r--r--toplevel/classes.ml2
-rw-r--r--toplevel/command.ml56
-rw-r--r--toplevel/himsg.ml62
-rw-r--r--toplevel/record.ml1
-rw-r--r--toplevel/vernacentries.ml2
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