aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml108
-rw-r--r--proofs/clenv.mli36
-rw-r--r--proofs/clenvtac.ml17
-rw-r--r--proofs/clenvtac.mli1
-rw-r--r--proofs/evar_refiner.ml20
-rw-r--r--proofs/goal.ml11
-rw-r--r--proofs/goal.mli12
-rw-r--r--proofs/logic.ml123
-rw-r--r--proofs/logic.mli6
-rw-r--r--proofs/pfedit.ml6
-rw-r--r--proofs/pfedit.mli12
-rw-r--r--proofs/proof.mli6
-rw-r--r--proofs/proof_global.ml5
-rw-r--r--proofs/proof_global.mli4
-rw-r--r--proofs/redexpr.ml13
-rw-r--r--proofs/redexpr.mli1
-rw-r--r--proofs/refine.ml7
-rw-r--r--proofs/refine.mli8
-rw-r--r--proofs/refiner.ml6
-rw-r--r--proofs/refiner.mli3
-rw-r--r--proofs/tacmach.ml24
-rw-r--r--proofs/tacmach.mli31
22 files changed, 259 insertions, 201 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index fad656223a..f9ebc42330 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -12,11 +12,12 @@ open Util
open Names
open Nameops
open Term
-open Vars
open Termops
open Namegen
open Environ
open Evd
+open EConstr
+open Vars
open Reduction
open Reductionops
open Tacred
@@ -43,12 +44,6 @@ type clausenv = {
let cl_env ce = ce.env
let cl_sigma ce = ce.evd
-let map_clenv sub clenv =
- { templval = map_fl sub clenv.templval;
- templtyp = map_fl sub clenv.templtyp;
- evd = cmap sub clenv.evd;
- env = clenv.env }
-
let clenv_nf_meta clenv c = nf_meta clenv.evd c
let clenv_term clenv c = meta_instance clenv.evd c
let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
@@ -56,9 +51,9 @@ let clenv_value clenv = meta_instance clenv.evd clenv.templval
let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
let refresh_undefined_univs clenv =
- match kind_of_term clenv.templval.rebus with
+ match EConstr.kind clenv.evd clenv.templval.rebus with
| Var _ -> clenv, Univ.empty_level_subst
- | App (f, args) when isVar f -> clenv, Univ.empty_level_subst
+ | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
| _ ->
let evd', subst = Evd.refresh_undefined_universes clenv.evd in
let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
@@ -71,15 +66,18 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
exception NotExtensibleClause
+let mk_freelisted c =
+ map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c))
+
let clenv_push_prod cl =
let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
- let rec clrec typ = match kind_of_term typ with
+ let rec clrec typ = match EConstr.kind cl.evd typ with
| Cast (t,_,_) -> clrec t
| Prod (na,t,u) ->
let mv = new_meta () in
- let dep = dependent (mkRel 1) u in
+ let dep = not (noccurn (cl_sigma cl) 1 u) in
let na' = if dep then na else Anonymous in
- let e' = meta_declare mv t ~name:na' cl.evd in
+ let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in
let concl = if dep then subst1 (mkMeta mv) u else u in
let def = applist (cl.templval.rebus,[mkMeta mv]) in
{ templval = mk_freelisted def;
@@ -103,14 +101,17 @@ let clenv_push_prod cl =
and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
let clenv_environments evd bound t =
+ let open EConstr in
+ let open Vars in
let rec clrec (e,metas) n t =
- match n, kind_of_term t with
+ match n, EConstr.kind evd t with
| (Some 0, _) -> (e, List.rev metas, t)
| (n, Cast (t,_,_)) -> clrec (e,metas) n t
| (n, Prod (na,t1,t2)) ->
let mv = new_meta () in
- let dep = not (noccurn 1 t2) in
+ let dep = not (noccurn evd 1 t2) in
let na' = if dep then na else Anonymous in
+ let t1 = EConstr.Unsafe.to_constr t1 in
let e' = meta_declare mv t1 ~name:na' e in
clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
(if dep then (subst1 (mkMeta mv) t2) else t2)
@@ -128,11 +129,13 @@ let mk_clenv_from_env env sigma n (c,cty) =
env = env }
let mk_clenv_from_n gls n (c,cty) =
- mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty)
+ let env = Proofview.Goal.env gls in
+ let sigma = Tacmach.New.project gls in
+ mk_clenv_from_env env sigma n (c, cty)
let mk_clenv_from gls = mk_clenv_from_n gls None
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t)
(******************************************************************)
@@ -168,13 +171,13 @@ let clenv_assign mv rhs clenv =
error "clenv_assign: circularity in unification";
try
if meta_defined clenv.evd mv then
- if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+ if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
error_incompatible_inst clenv mv
else
clenv
else
let st = (Conv,TypeNotProcessed) in
- {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
+ {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
with Not_found ->
error "clenv_assign: undefined meta"
@@ -219,7 +222,7 @@ let clenv_assign mv rhs clenv =
*)
let clenv_metas_in_type_of_meta evd mv =
- (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
+ (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas
let dependent_in_type_of_metas clenv mvs =
List.fold_right
@@ -262,35 +265,38 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
{ clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
-let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
- let concl = Goal.V82.concl clenv.evd (sig_it gl) in
- if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then
+let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
+ if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
clenv_unify CUMUL ~flags (clenv_type clenv) concl
(clenv_unify_meta_types ~flags clenv)
else
clenv_unify CUMUL ~flags
(meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
+let old_clenv_unique_resolver ?flags clenv gl =
+ let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+ clenv_unique_resolver_gen ?flags clenv concl
+
+let clenv_unique_resolver ?flags clenv gl =
+ let concl = Proofview.Goal.concl gl in
+ clenv_unique_resolver_gen ?flags clenv concl
+
let adjust_meta_source evd mv = function
| loc,Evar_kinds.VarInstance id ->
let rec match_name c l =
- match kind_of_term c, l with
- | Lambda (Name id,_,c), a::l when Constr.equal a (mkMeta mv) -> Some id
+ match EConstr.kind evd c, l with
+ | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id
| Lambda (_,_,c), a::l -> match_name c l
| _ -> None in
(* This is very ad hoc code so that an evar inherits the name of the binder
in situations like "ex_intro (fun x => P) ?ev p" *)
let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
if Metaset.mem mv t.freemetas then
- let f,l = decompose_app t.rebus in
- match kind_of_term f with
+ let f,l = decompose_app evd (EConstr.of_constr t.rebus) in
+ match EConstr.kind evd f with
| Meta mv'' ->
(match meta_opt_fvalue evd mv'' with
- | Some (c,_) -> match_name c.rebus l
- | None -> None)
- | Evar ev ->
- (match existential_opt_value evd ev with
- | Some c -> match_name c l
+ | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l
| None -> None)
| _ -> None
else None in
@@ -332,7 +338,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
let ty = clenv_meta_type clenv mv in
(* Postpone the evar-ization if dependent on another meta *)
(* This assumes no cycle in the dependencies - is it correct ? *)
- if occur_meta ty then fold clenv (mvs@[mv])
+ if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
else
let src = evar_source_of_meta mv clenv.evd in
let src = adjust_meta_source clenv.evd mv src in
@@ -404,7 +410,7 @@ type arg_bindings = constr explicit_bindings
* of cval, ctyp. *)
let clenv_independent clenv =
- let mvs = collect_metas (clenv_value clenv) in
+ let mvs = collect_metas clenv.evd (clenv_value clenv) in
let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
@@ -482,7 +488,7 @@ let error_already_defined b =
(str "Position " ++ int n ++ str" already defined.")
let clenv_unify_binding_type clenv c t u =
- if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
+ if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then
(* Not enough information to know if some subtyping is needed *)
CoerceToType, clenv, c
else
@@ -501,6 +507,7 @@ let clenv_assign_binding clenv k c =
let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
+ let c = EConstr.Unsafe.to_constr c in
{ clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
let clenv_match_args bl clenv =
@@ -513,7 +520,7 @@ let clenv_match_args bl clenv =
(fun clenv (loc,b,c) ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
- if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+ if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
else error_already_defined b
else
clenv_assign_binding clenv k c)
@@ -522,7 +529,7 @@ let clenv_match_args bl clenv =
exception NoSuchBinding
let clenv_constrain_last_binding c clenv =
- let all_mvs = collect_metas clenv.templval.rebus in
+ let all_mvs = collect_metas clenv.evd clenv.templval.rebus in
let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
clenv_assign_binding clenv k c
@@ -557,8 +564,9 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
let clause = mk_clenv_from_env env sigma n (c,t) in
clenv_constrain_dep_args hyps_only largs clause
| ExplicitBindings lbind ->
+ let t = rename_bound_vars_as_displayed sigma [] [] t in
let clause = mk_clenv_from_env env sigma n
- (c,rename_bound_vars_as_displayed [] [] t)
+ (c, t)
in clenv_match_args lbind clause
| NoBindings ->
mk_clenv_from_env env sigma n (c,t)
@@ -585,34 +593,36 @@ let pr_clenv clenv =
(** Evar version of mk_clenv *)
type hole = {
- hole_evar : constr;
- hole_type : types;
+ hole_evar : EConstr.constr;
+ hole_type : EConstr.types;
hole_deps : bool;
hole_name : Name.t;
}
type clause = {
cl_holes : hole list;
- cl_concl : types;
+ cl_concl : EConstr.types;
}
let make_evar_clause env sigma ?len t =
+ let open EConstr in
+ let open Vars in
let bound = match len with
| None -> -1
| Some n -> assert (0 <= n); n
in
(** FIXME: do the renaming online *)
- let t = rename_bound_vars_as_displayed [] [] t in
+ let t = rename_bound_vars_as_displayed sigma [] [] t in
let rec clrec (sigma, holes) n t =
if n = 0 then (sigma, holes, t)
- else match kind_of_term t with
+ else match EConstr.kind sigma t with
| Cast (t, _, _) -> clrec (sigma, holes) n t
| Prod (na, t1, t2) ->
let store = Typeclasses.set_resolvable Evd.Store.empty false in
let sigma = Sigma.Unsafe.of_evar_map sigma in
let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
let sigma = Sigma.to_evar_map sigma in
- let dep = dependent (mkRel 1) t2 in
+ let dep = not (noccurn sigma 1 t2) in
let hole = {
hole_evar = ev;
hole_type = t1;
@@ -667,24 +677,26 @@ let evar_of_binder holes = function
user_err (str "No such binder.")
let define_with_type sigma env ev c =
+ let open EConstr in
let t = Retyping.get_type_of env sigma ev in
let ty = Retyping.get_type_of env sigma c in
let j = Environ.make_judge c ty in
let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
- let (ev, _) = destEvar ev in
- let sigma = Evd.define ev j.Environ.uj_val sigma in
+ let (ev, _) = destEvar sigma ev in
+ let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
sigma
let solve_evar_clause env sigma hyp_only clause = function
| NoBindings -> sigma
| ImplicitBindings largs ->
+ let open EConstr in
let fold holes h =
if h.hole_deps then
(** Some subsequent term uses the hole *)
- let (ev, _) = destEvar h.hole_evar in
- let is_dep hole = occur_evar ev hole.hole_type in
+ let (ev, _) = destEvar sigma h.hole_evar in
+ let is_dep hole = occur_evar sigma ev hole.hole_type in
let in_hyp = List.exists is_dep holes in
- let in_ccl = occur_evar ev clause.cl_concl in
+ let in_ccl = occur_evar sigma ev clause.cl_concl in
let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in
let h = { h with hole_deps = dep } in
h :: holes
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index e9236b1da3..4bcd50591c 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -14,6 +14,7 @@ open Names
open Term
open Environ
open Evd
+open EConstr
open Unification
open Misctypes
@@ -28,8 +29,6 @@ type clausenv = {
templtyp : constr freelisted (** its type *)}
-val map_clenv : (constr -> constr) -> clausenv -> clausenv
-
(** subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
@@ -37,16 +36,16 @@ val clenv_value : clausenv -> constr
val clenv_type : clausenv -> types
(** substitute resolved metas *)
-val clenv_nf_meta : clausenv -> constr -> constr
+val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr
(** type of a meta in clenv context *)
val clenv_meta_type : clausenv -> metavariable -> types
-val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv
+val mk_clenv_from : ('a, 'r) Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
val mk_clenv_from_n :
- Goal.goal sigma -> int option -> constr * types -> clausenv
-val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
-val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
+ ('a, 'r) Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> clausenv
+val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
(** Refresh the universes in a clenv *)
val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
@@ -63,9 +62,12 @@ val clenv_unify :
?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
(** unifies the concl of the goal with the type of the clenv *)
-val clenv_unique_resolver :
+val old_clenv_unique_resolver :
?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
+val clenv_unique_resolver :
+ ?flags:unify_flags -> clausenv -> ('a, 'r) Proofview.Goal.t -> clausenv
+
val clenv_dependent : clausenv -> metavariable list
val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
@@ -92,18 +94,18 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
the optional int tells how many prods of the lemma have to be used
use all of them if None *)
val make_clenv_binding_env_apply :
- env -> evar_map -> int option -> constr * constr -> constr bindings ->
+ env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
clausenv
val make_clenv_binding_apply :
- env -> evar_map -> int option -> constr * constr -> constr bindings ->
+ env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
clausenv
val make_clenv_binding_env :
- env -> evar_map -> constr * constr -> constr bindings -> clausenv
+ env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
val make_clenv_binding :
- env -> evar_map -> constr * constr -> constr bindings -> clausenv
+ env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
(** if the clause is a product, add an extra meta for this product *)
exception NotExtensibleClause
@@ -134,9 +136,9 @@ val pr_clenv : clausenv -> Pp.std_ppcmds
*)
type hole = {
- hole_evar : constr;
+ hole_evar : EConstr.constr;
(** The hole itself. Guaranteed to be an evar. *)
- hole_type : types;
+ hole_type : EConstr.types;
(** Type of the hole in the current environment. *)
hole_deps : bool;
(** Whether the remainder of the clause was dependent in the hole. Note that
@@ -148,10 +150,10 @@ type hole = {
type clause = {
cl_holes : hole list;
- cl_concl : types;
+ cl_concl : EConstr.types;
}
-val make_evar_clause : env -> evar_map -> ?len:int -> types ->
+val make_evar_clause : env -> evar_map -> ?len:int -> EConstr.types ->
(evar_map * clause)
(** An evar version of {!make_clenv_binding}. Given a type [t],
[evar_environments env sigma ~len t bl] tries to eliminate at most [len]
@@ -159,7 +161,7 @@ val make_evar_clause : env -> evar_map -> ?len:int -> types ->
type together with the list of holes generated. Assumes that [t] is
well-typed in the environment. *)
-val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
+val solve_evar_clause : env -> evar_map -> bool -> clause -> EConstr.constr bindings ->
evar_map
(** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained
in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 98b5bc8b05..0722ea0470 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -11,6 +11,7 @@ open Names
open Term
open Termops
open Evd
+open EConstr
open Refiner
open Logic
open Reduction
@@ -26,19 +27,19 @@ open Proofview.Notations
let clenv_cast_meta clenv =
let rec crec u =
- match kind_of_term u with
+ match EConstr.kind clenv.evd u with
| App _ | Case _ -> crec_hd u
- | Cast (c,_,_) when isMeta c -> u
+ | Cast (c,_,_) when isMeta clenv.evd c -> u
| Proj (p, c) -> mkProj (p, crec_hd c)
- | _ -> map_constr crec u
+ | _ -> EConstr.map clenv.evd crec u
and crec_hd u =
- match kind_of_term (strip_outer_cast u) with
+ match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with
| Meta mv ->
(try
let b = Typing.meta_type clenv.evd mv in
- assert (not (occur_meta b));
- if occur_meta b then u
+ assert (not (occur_meta clenv.evd b));
+ if occur_meta clenv.evd b then u
else mkCast (mkMeta mv, DEFAULTcast, b)
with Not_found -> u)
| App(f,args) -> mkApp (crec_hd f, Array.map crec args)
@@ -104,8 +105,8 @@ let dft = default_unify_flags
let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
Proofview.Goal.enter { enter = begin fun gl ->
- let clenv gl = clenv_unique_resolver ~flags clenv gl in
- clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
+ let clenv = clenv_unique_resolver ~flags clenv gl in
+ clenv_refine with_evars ~with_classes clenv
end }
(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 8a096b6457..5b7164705a 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -10,6 +10,7 @@
open Term
open Clenv
+open EConstr
open Unification
open Misctypes
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 509efbc5b8..8367c09b8f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -18,21 +18,23 @@ open Pp
(* Instantiation of existential variables *)
(******************************************)
-let depends_on_evar evk _ (pbty,_,t1,t2) =
- try Evar.equal (head_evar t1) evk
+let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
+ let t1 = EConstr.of_constr t1 in
+ let t2 = EConstr.of_constr t2 in
+ try Evar.equal (head_evar sigma t1) evk
with NoHeadEvar ->
- try Evar.equal (head_evar t2) evk
+ try Evar.equal (head_evar sigma t2) evk
with NoHeadEvar -> false
let define_and_solve_constraints evk c env evd =
- if Termops.occur_evar evk c then
+ if Termops.occur_evar evd evk c then
Pretype_errors.error_occur_check env evd evk c;
- let evd = define evk c evd in
- let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
+ let evd = define evk (EConstr.Unsafe.to_constr c) evd in
+ let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in
match
List.fold_left
(fun p (pbty,env,t1,t2) -> match p with
- | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2
+ | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2)
| UnifFailure _ as x -> x) (Success evd)
pbs
with
@@ -51,11 +53,11 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
Pretyping.fail_evar = false;
Pretyping.expand_evars = true } in
try Pretyping.understand_ltac flags
- env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
+ env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
with e when CErrors.noncritical e ->
let loc = Glob_ops.loc_of_glob_constr rawc in
user_err ~loc
(str "Instance is not well-typed in the environment of " ++
- pr_existential_key sigma evk ++ str ".")
+ Termops.pr_existential_key sigma evk ++ str ".")
in
define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index a141708c2b..9046f45341 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -49,7 +49,7 @@ module V82 = struct
(* Access to ".evar_concl" *)
let concl evars gl =
let evi = Evd.find evars gl in
- evi.Evd.evar_concl
+ EConstr.of_constr evi.Evd.evar_concl
(* Access to ".evar_extra" *)
let extra evars gl =
@@ -62,6 +62,7 @@ module V82 = struct
be shelved. It must not appear as a future_goal, so the future
goals are restored to their initial value after the evar is
created. *)
+ let concl = EConstr.Unsafe.to_constr concl in
let prev_future_goals = Evd.future_goals evars in
let prev_principal_goal = Evd.principal_future_goal evars in
let evi = { Evd.evar_hyps = hyps;
@@ -78,8 +79,8 @@ module V82 = struct
let evars = Sigma.to_evar_map evars in
let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
let ctxt = Environ.named_context_of_val hyps in
- let inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
- let ev = Term.mkEvar (evk,inst) in
+ let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
+ let ev = EConstr.mkEvar (evk,inst) in
(evk, ev, evars)
(* Instantiates a goal with an open term *)
@@ -89,7 +90,7 @@ module V82 = struct
if not (Evarutil.occur_evar_upto sigma evk c) then ()
else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
in
- Evd.define evk c sigma
+ Evd.define evk (EConstr.Unsafe.to_constr c) sigma
(* Instantiates a goal with an open term, using name of goal for evk' *)
let partial_solution_to sigma evk evk' c =
@@ -145,6 +146,7 @@ module V82 = struct
(* Goal represented as a type, doesn't take into account section variables *)
let abstract_type sigma gl =
+ let open EConstr in
let (gl,sigma) = nf_evar sigma gl in
let env = env sigma gl in
let genv = Global.env () in
@@ -153,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/goal.mli b/proofs/goal.mli
index 6a79c1f451..a2fa34c05e 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -38,7 +38,7 @@ module V82 : sig
val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val
(* Access to ".evar_concl" *)
- val concl : Evd.evar_map -> goal -> Term.constr
+ val concl : Evd.evar_map -> goal -> EConstr.constr
(* Access to ".evar_extra" *)
val extra : Evd.evar_map -> goal -> Evd.Store.t
@@ -48,16 +48,16 @@ module V82 : sig
the evar corresponding to the goal, and an updated evar_map. *)
val mk_goal : Evd.evar_map ->
Environ.named_context_val ->
- Term.constr ->
+ EConstr.constr ->
Evd.Store.t ->
- goal * Term.constr * Evd.evar_map
+ goal * EConstr.constr * Evd.evar_map
(* Instantiates a goal with an open term *)
- val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
+ val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
(* Instantiates a goal with an open term, reusing name of goal for
second goal *)
- val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map
+ val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
(* Principal part of the weak-progress tactical *)
val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
@@ -75,6 +75,6 @@ module V82 : sig
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
(* Goal represented as a type, doesn't take into account section variables *)
- val abstract_type : Evd.evar_map -> goal -> Term.types
+ val abstract_type : Evd.evar_map -> goal -> EConstr.types
end
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 44c6294841..e6024785db 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -34,7 +34,7 @@ type refiner_error =
| CannotApply of constr * constr
| NotWellTyped of constr
| NonLinearProof of constr
- | MetaInType of constr
+ | MetaInType of EConstr.constr
(* Errors raised by the tactics *)
| IntroNeedsProduct
@@ -86,7 +86,7 @@ let apply_to_hyp check sign id f =
else sign
let check_typability env sigma c =
- if !check then let _ = unsafe_type_of env sigma c in ()
+ if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
(************************************************************************)
(************************************************************************)
@@ -138,12 +138,12 @@ let find_q x (m,q) =
else find (Id.Set.union l accs) (i::acc) itl in
find Id.Set.empty [] q
-let occur_vars_in_decl env hyps d =
+let occur_vars_in_decl env sigma hyps d =
if Id.Set.is_empty hyps then false else
- let ohyps = global_vars_set_of_decl env d in
+ let ohyps = global_vars_set_of_decl env sigma d in
Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps
-let reorder_context env sign ord =
+let reorder_context env sigma sign ord =
let ords = List.fold_right Id.Set.add ord Id.Set.empty in
if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then
error "Order list has duplicates";
@@ -152,13 +152,13 @@ let reorder_context env sign ord =
| [] -> List.rev ctxt_tail @ ctxt_head
| top::ord' when mem_q top moved_hyps ->
let ((d,h),mh) = find_q top moved_hyps in
- if occur_vars_in_decl env h d then
+ if occur_vars_in_decl env sigma h d then
user_err ~hdr:"reorder_context"
(str "Cannot move declaration " ++ pr_id top ++ spc() ++
str "before " ++
pr_sequence pr_id
(Id.Set.elements (Id.Set.inter h
- (global_vars_set_of_decl env d))));
+ (global_vars_set_of_decl env sigma d))));
step ord' expected ctxt_head mh (d::ctxt_tail)
| _ ->
(match ctxt_head with
@@ -173,16 +173,18 @@ let reorder_context env sign ord =
ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
step ord ords sign mt_q []
-let reorder_val_context env sign ord =
- val_of_named_context (reorder_context env (named_context_of_val sign) ord)
+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 sign d =
+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 d in
- let deps = dependency_closure env (named_context_of_val sign) needed 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
if Id.List.mem x deps then
user_err ~hdr:"Logic.check_decl_position"
(str "Cannot create self-referring hypothesis " ++ pr_id x);
@@ -233,12 +235,12 @@ let hyp_of_move_location = function
| MoveBefore id -> id
| _ -> assert false
-let move_hyp toleft (left,declfrom,right) hto =
+let move_hyp sigma toleft (left,declfrom,right) hto =
let env = Global.env() in
let test_dep d d2 =
if toleft
- then occur_var_in_decl env (NamedDecl.get_id d2) d
- else occur_var_in_decl env (NamedDecl.get_id d) d2
+ then occur_var_in_decl env sigma (NamedDecl.get_id d2) d
+ else occur_var_in_decl env sigma (NamedDecl.get_id d) d2
in
let rec moverec first middle = function
| [] ->
@@ -266,6 +268,7 @@ let move_hyp 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
@@ -278,10 +281,11 @@ let move_hyp toleft (left,declfrom,right) hto =
List.fold_left (fun sign d -> push_named_context_val d sign)
right left
-let move_hyp_in_named_context hfrom hto sign =
+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 toleft (left,declfrom,right) hto
+ move_hyp sigma toleft (left,declfrom,right) hto
(**********************************************************************)
@@ -314,23 +318,26 @@ let check_meta_variables c =
let check_conv_leq_goal env sigma arg ty conclty =
if !check then
- let evm, b = Reductionops.infer_conv env sigma ty conclty in
+ let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
if b then evm
else raise (RefinerError (BadType (arg,ty,conclty)))
else sigma
-exception Stop of constr list
-let meta_free_prefix a =
+exception Stop of EConstr.t list
+let meta_free_prefix sigma a =
try
+ let a = Array.map EConstr.of_constr a in
let _ = Array.fold_left (fun acc a ->
- if occur_meta a then raise (Stop acc)
+ if occur_meta sigma a then raise (Stop acc)
else a :: acc) [] a
in a
with Stop acc -> Array.rev_of_list acc
let goal_type_of env sigma c =
- if !check then unsafe_type_of env sigma c
- else Retyping.get_type_of env sigma c
+ if !check then
+ let (sigma,t) = type_of env sigma (EConstr.of_constr c) in
+ (sigma, EConstr.Unsafe.to_constr t)
+ else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)))
let rec mk_refgoals sigma goal goalacc conclty trm =
let env = Goal.V82.env sigma goal in
@@ -338,17 +345,20 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let mk_goal hyps concl =
Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
in
- if (not !check) && not (occur_meta trm) then
- let t'ty = Retyping.get_type_of env sigma trm in
+ if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
+ let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in
+ let t'ty = EConstr.Unsafe.to_constr t'ty in
let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
(goalacc,t'ty,sigma,trm)
else
match kind_of_term trm with
| Meta _ ->
- let conclty = nf_betaiota sigma conclty in
- if !check && occur_meta conclty then
+ let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
+ if !check && occur_meta sigma conclty then
raise (RefinerError (MetaInType conclty));
let (gl,ev,sigma) = mk_goal hyps conclty in
+ let ev = EConstr.Unsafe.to_constr ev in
+ let conclty = EConstr.Unsafe.to_constr conclty in
gl::goalacc, conclty, sigma, ev
| Cast (t,k, ty) ->
@@ -367,13 +377,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| App (f,l) ->
let (acc',hdty,sigma,applicand) =
- if is_template_polymorphic env f then
+ if is_template_polymorphic env sigma (EConstr.of_constr f) then
let ty =
(* Template sort-polymorphism of definition and inductive types *)
- let firstmeta = Array.findi (fun i x -> occur_meta x) l in
+ let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
- type_of_global_reference_knowing_parameters env sigma f args
+ type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args)
in
+ let ty = EConstr.Unsafe.to_constr ty in
goalacc, ty, sigma, f
else
mk_hdgoals sigma goal goalacc f
@@ -386,7 +397,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| Proj (p,c) ->
let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
let c = mkProj (p, c') in
- let ty = get_type_of env sigma c in
+ let ty = get_type_of env sigma (EConstr.of_constr c) in
+ let ty = EConstr.Unsafe.to_constr ty in
(acc',ty,sigma,c)
| Case (ci,p,c,lf) ->
@@ -406,9 +418,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
(acc'',conclty',sigma, ans)
| _ ->
- if occur_meta trm then
+ if occur_meta sigma (EConstr.of_constr trm) then
anomaly (Pp.str "refiner called with a meta in non app/case subterm");
- let t'ty = goal_type_of env sigma trm in
+ let (sigma, t'ty) = goal_type_of env sigma trm in
let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
(goalacc,t'ty,sigma, trm)
@@ -423,7 +435,8 @@ and mk_hdgoals sigma goal goalacc trm =
match kind_of_term trm with
| Cast (c,_, ty) when isMeta c ->
check_typability env sigma ty;
- let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma ty) in
+ let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
+ let ev = EConstr.Unsafe.to_constr ev in
gl::goalacc,ty,sigma,ev
| Cast (t,_, ty) ->
@@ -432,10 +445,10 @@ and mk_hdgoals sigma goal goalacc trm =
| App (f,l) ->
let (acc',hdty,sigma,applicand) =
- if is_template_polymorphic env f
+ if is_template_polymorphic env sigma (EConstr.of_constr f)
then
- let l' = meta_free_prefix l in
- (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f)
+ let l' = meta_free_prefix sigma l in
+ (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
else mk_hdgoals sigma goal goalacc f
in
let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
@@ -460,17 +473,20 @@ and mk_hdgoals sigma goal goalacc trm =
| Proj (p,c) ->
let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
let c = mkProj (p, c') in
- let ty = get_type_of env sigma c in
+ let ty = get_type_of env sigma (EConstr.of_constr c) in
+ let ty = EConstr.Unsafe.to_constr ty in
(acc',ty,sigma,c)
| _ ->
- if !check && occur_meta trm then
+ if !check && occur_meta sigma (EConstr.of_constr trm) then
anomaly (Pp.str "refine called with a dependent meta");
- goalacc, goal_type_of env sigma trm, sigma, trm
+ let (sigma, ty) = goal_type_of env sigma trm in
+ goalacc, ty, sigma, trm
and mk_arggoals sigma goal goalacc funty allargs =
let foldmap (goalacc, funty, sigma) harg =
- let t = whd_all (Goal.V82.env sigma goal) sigma funty in
+ let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
+ let t = EConstr.Unsafe.to_constr t in
let rec collapse t = match kind_of_term t with
| LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
| _ -> t
@@ -487,11 +503,13 @@ and mk_arggoals sigma goal goalacc funty allargs =
and mk_casegoals sigma goal goalacc p c =
let env = Goal.V82.env sigma goal in
let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
+ let ct = EConstr.of_constr ct in
let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
- let indspec =
+ let ((ind, u), spec) =
try Tacred.find_hnf_rectype env sigma ct
with Not_found -> anomaly (Pp.str "mk_casegoals") in
- let (lbrty,conclty) = type_case_branches_with_names env indspec p c in
+ let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in
+ let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
(acc'',lbrty,conclty,sigma,p',c')
@@ -503,17 +521,17 @@ let convert_hyp check sign sigma d =
let sign' =
apply_to_hyp check sign id
(fun _ d' _ ->
- let c = NamedDecl.get_value d' in
+ 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 (NamedDecl.get_type d) (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 sign d;
- d) in
- reorder_val_context env sign' !reorder
+ if check then reorder := check_decl_position env sigma sign d;
+ map_named_decl EConstr.Unsafe.to_constr d) in
+ reorder_val_context env sigma sign' !reorder
@@ -528,16 +546,18 @@ let prim_refiner r sigma goal =
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 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
let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in
- move_hyp false ([], LocalAssum (id,t),named_context_of_val sign)
+ move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign)
nexthyp,
t,cl,sigma
else
@@ -547,13 +567,14 @@ let prim_refiner r sigma goal =
push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
let (sg2,ev2,sigma) =
Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
- let oterm = Term.mkNamedLetIn id ev1 t ev2 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
- let sigma = Goal.V82.partial_solution sigma goal oterm in
+ let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in
(sgl, sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 0dba9ef1ee..f98248e4d1 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -43,7 +43,7 @@ type refiner_error =
| CannotApply of constr * constr
| NotWellTyped of constr
| NonLinearProof of constr
- | MetaInType of constr
+ | MetaInType of EConstr.constr
(*i Errors raised by the tactics i*)
| IntroNeedsProduct
@@ -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 : Id.t -> Id.t Misctypes.move_location ->
+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/pfedit.ml b/proofs/pfedit.ml
index 9995a9394a..7e8ed31d1d 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -210,6 +210,7 @@ let refine_by_tactic env sigma ty tac =
| _ -> assert false
in
let ans = Reductionops.nf_evar sigma ans in
+ let ans = EConstr.Unsafe.to_constr ans in
(** [neff] contains the freshly generated side-effects *)
let neff = Evd.eval_side_effects sigma in
(** Reset the old side-effects *)
@@ -238,16 +239,17 @@ let apply_implicit_tactic tac = (); fun env sigma evk ->
match snd (evar_source evk sigma) with
| (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
when
- Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
+ Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
(try
let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
+ let c = EConstr.of_constr c in
if Evarutil.has_undefined_evars sigma c then raise Exit;
let (ans, _, ctx) =
build_by_tactic env (Evd.evar_universe_context sigma) c tac in
let sigma = Evd.set_universe_context sigma ctx in
- sigma, ans
+ sigma, EConstr.of_constr ans
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index aad719db49..f9fb0b76de 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -60,7 +60,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards
type universe_binders = Id.t Loc.located list
val start_proof :
- Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
+ Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
?init_tac:unit Proofview.tactic ->
Proof_global.proof_terminator -> unit
@@ -106,7 +106,7 @@ val get_current_context : unit -> Evd.evar_map * env
(** [current_proof_statement] *)
val current_proof_statement :
- unit -> Id.t * goal_kind * types
+ unit -> Id.t * goal_kind * EConstr.types
(** {6 ... } *)
(** [get_current_proof_name ()] return the name of the current focused
@@ -166,15 +166,15 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
val build_constant_by_tactic :
Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
- types -> unit Proofview.tactic ->
+ EConstr.types -> unit Proofview.tactic ->
Safe_typing.private_constants Entries.definition_entry * bool *
Evd.evar_universe_context
val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
- types -> unit Proofview.tactic ->
+ EConstr.types -> unit Proofview.tactic ->
constr * bool * Evd.evar_universe_context
-val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic ->
+val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
constr * Evd.evar_map
(** A variant of the above function that handles open terms as well.
Caveat: all effects are purged in the returned term at the end, but other
@@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
val clear_implicit_tactic : unit -> unit
(* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr) option
+val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr) option
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 8dc165e72e..9d38e16ad7 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -66,9 +66,9 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
(*** General proof functions ***)
-val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
+val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
val dependent_start : Proofview.telescope -> proof
-val initial_goals : proof -> (Term.constr * Term.types) list
+val initial_goals : proof -> (EConstr.constr * EConstr.types) list
val initial_euctx : proof -> Evd.evar_universe_context
(* Returns [true] if the considered proof is completed, that is if no goal remain
@@ -79,7 +79,7 @@ val is_done : proof -> bool
val is_complete : proof -> bool
(* Returns the list of partial proofs to initial goals. *)
-val partial_proof : proof -> Term.constr list
+val partial_proof : proof -> EConstr.constr list
val compact : proof -> proof
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ca7330fdb6..e4cba6f07d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -378,6 +378,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
in
let entries =
Future.map2 (fun p (_, t) ->
+ let t = EConstr.Unsafe.to_constr t in
let univstyp, body = make_body t p in
let univs, typ = Future.force univstyp in
{ Entries.
@@ -407,7 +408,7 @@ let return_proof ?(allow_partial=false) () =
(** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
side-effects... This may explain why one need to uniquize side-effects
thereafter... *)
- let proofs = List.map (fun c -> c, eff) proofs in
+ let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
proofs, Evd.evar_universe_context evd
end else
let initial_goals = Proof.initial_goals proof in
@@ -431,7 +432,7 @@ let return_proof ?(allow_partial=false) () =
side-effects... This may explain why one need to uniquize side-effects
thereafter... *)
let proofs =
- List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in
+ List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in
proofs, Evd.evar_universe_context evd
let close_future_proof ~feedback_id proof =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 97a21cf225..3b2cc6b23b 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -86,7 +86,7 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
end of the proof to close the proof. *)
val start_proof :
Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
- Decl_kinds.goal_kind -> (Environ.env * Term.types) list ->
+ Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list ->
proof_terminator -> unit
(** Like [start_proof] except that there may be dependencies between
@@ -201,7 +201,7 @@ end
val get_default_goal_selector : unit -> Vernacexpr.goal_selector
module V82 : sig
- val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
+ val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
Decl_kinds.goal_kind)
end
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 34443b93da..0fe5c73f15 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -11,6 +11,7 @@ open CErrors
open Util
open Names
open Term
+open EConstr
open Declarations
open Globnames
open Genredexpr
@@ -25,9 +26,7 @@ open Misctypes
(* call by value normalisation function using the virtual machine *)
let cbv_vm env sigma c =
let ctyp = Retyping.get_type_of env sigma c in
- if Termops.occur_meta_or_existential c then
- error "vm_compute does not support existential variables.";
- Vnorm.cbv_vm env c ctyp
+ Vnorm.cbv_vm env sigma c ctyp
let warn_native_compute_disabled =
CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
@@ -45,7 +44,8 @@ let cbv_native env sigma c =
let whd_cbn flags env sigma t =
let (state,_) =
(whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
- in Reductionops.Stack.zip ~refold:true state
+ in
+ Reductionops.Stack.zip ~refold:true sigma state
let strong_cbn flags =
strong (whd_cbn flags)
@@ -254,9 +254,12 @@ let reduction_of_red_expr env =
in
reduction_of_red_expr
+let subst_mps subst c =
+ EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
+
let subst_red_expr subs =
Miscops.map_red_expr_gen
- (Mod_subst.subst_mps subs)
+ (subst_mps subs)
(Mod_subst.subst_evaluable_reference subs)
(Patternops.subst_pattern subs)
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index d4c2c4a6c9..45e4610661 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -10,6 +10,7 @@
open Names
open Term
+open EConstr
open Pattern
open Genredexpr
open Reductionops
diff --git a/proofs/refine.ml b/proofs/refine.ml
index c238f731d5..1ee6e0ca5f 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -28,12 +28,12 @@ let typecheck_evar ev env sigma =
let info = Evd.find sigma ev in
(** Typecheck the hypotheses. *)
let type_hyp (sigma, env) decl =
- let t = NamedDecl.get_type decl in
+ let t = EConstr.of_constr (NamedDecl.get_type decl) in
let evdref = ref sigma in
let _ = Typing.e_sort_of env evdref t in
let () = match decl with
| LocalAssum _ -> ()
- | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+ | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
in
(!evdref, Environ.push_named decl env)
in
@@ -42,7 +42,7 @@ let typecheck_evar ev env sigma =
let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
(** Typecheck the conclusion *)
let evdref = ref sigma in
- let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
+ let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
!evdref
let typecheck_proof c concl env sigma =
@@ -101,6 +101,7 @@ let make_refine_enter ?(unsafe = true) f =
else Pretype_errors.error_occur_check env sigma self c
in
(** Proceed to the refinement *)
+ let c = EConstr.Unsafe.to_constr c in
let sigma = match evkmain with
| None -> Evd.define self c sigma
| Some evk ->
diff --git a/proofs/refine.mli b/proofs/refine.mli
index a44632eff5..1a254d578c 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -21,7 +21,7 @@ val pr_constr :
(** {7 Refinement primitives} *)
-val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
(** In [refine ?unsafe t], [t] is a term with holes under some
[evar_map] context. The term [t] is used as a partial solution
for the current goal (refine is a goal-dependent tactic), the
@@ -30,17 +30,17 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
tactic failures. If [unsafe] is [false] (default is [true]) [t] is
type-checked beforehand. *)
-val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
+val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
(** A generalization of [refine] which assumes exactly one goal under focus *)
(** {7 Helper functions} *)
val with_type : Environ.env -> Evd.evar_map ->
- Term.constr -> Term.types -> Evd.evar_map * Term.constr
+ EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr
(** [with_type env sigma c t] ensures that [c] is of type [t]
inserting a coercion if needed. *)
-val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine_casted : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
(** Like {!refine} except the refined term is coerced to the conclusion of the
current goal. *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 9a0b56b84b..5c7659ac0e 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 6dcafb77a4..56f5facf89 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 030a3cbfb9..b55f8ef113 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -41,11 +41,14 @@ let project = Refiner.project
let pf_env = Refiner.pf_env
let pf_hyps = Refiner.pf_hyps
+let test_conversion env sigma pb c1 c2 =
+ Reductionops.check_conv ~pb env sigma c1 c2
+
let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
let pf_hyps_types gls =
let sign = Environ.named_context (pf_env gls) in
List.map (function LocalAssum (id,x)
- | LocalDef (id,_,x) -> id, x)
+ | LocalDef (id,_,x) -> id, EConstr.of_constr x)
sign
let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id
@@ -72,7 +75,7 @@ let pf_get_new_ids ids gls =
(fun id acc -> (next_ident_away id (acc@avoid))::acc)
ids []
-let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
+let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id)
let pf_reduction_of_red_expr gls re c =
let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
@@ -98,15 +101,15 @@ let pf_get_type_of = pf_reduce Retyping.get_type_of
let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV
let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL
-let pf_const_value = pf_reduce (fun env _ -> constant_value_in env)
+let pf_const_value = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c))
let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind
let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls
-let pf_is_matching = pf_apply Constr_matching.is_matching_conv
-let pf_matches = pf_apply Constr_matching.matches_conv
+let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c
+let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c
(********************************************)
(* Definition of the most primitive tactics *)
@@ -115,12 +118,15 @@ let pf_matches = pf_apply Constr_matching.matches_conv
let refiner = refiner
let internal_cut_no_check replace id t gl =
+ let t = EConstr.Unsafe.to_constr t in
refiner (Cut (true,replace,id,t)) gl
let internal_cut_rev_no_check replace id t gl =
+ let t = EConstr.Unsafe.to_constr t in
refiner (Cut (false,replace,id,t)) gl
let refine_no_check c gl =
+ let c = EConstr.Unsafe.to_constr c in
refiner (Refine c) gl
(* Versions with consistency checks *)
@@ -136,7 +142,7 @@ open Pp
let db_pr_goal sigma g =
let env = Goal.V82.env sigma g in
let penv = print_named_context env in
- let pc = print_constr_env env (Goal.V82.concl sigma g) in
+ let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in
str" " ++ hv 0 (penv ++ fnl () ++
str "============================" ++ fnl () ++
str" " ++ pc) ++ fnl ()
@@ -165,7 +171,7 @@ module New = struct
(** We only check for the existence of an [id] in [hyps] *)
let gl = Proofview.Goal.assume gl in
let hyps = Proofview.Goal.hyps gl in
- Constrintern.construct_reference hyps id
+ EConstr.of_constr (Constrintern.construct_reference hyps id)
let pf_env = Proofview.Goal.env
let pf_concl = Proofview.Goal.concl
@@ -194,7 +200,7 @@ 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
@@ -206,7 +212,7 @@ module New = struct
let env = Proofview.Goal.env gl in
let sign = Environ.named_context env in
List.map (function LocalAssum (id,x)
- | LocalDef (id,_,x) -> id, x)
+ | LocalDef (id,_,x) -> id, EConstr.of_constr x)
sign
let pf_last_hyp gl =
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 59f296f64e..627a8e0e7e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -9,6 +9,7 @@
open Names
open Term
open Environ
+open EConstr
open Evd
open Proof_type
open Redexpr
@@ -33,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
@@ -67,8 +68,8 @@ val pf_whd_all : goal sigma -> constr -> constr
val pf_hnf_constr : goal sigma -> constr -> constr
val pf_nf : goal sigma -> constr -> constr
val pf_nf_betaiota : goal sigma -> constr -> constr
-val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types
-val pf_reduce_to_atomic_ind : goal sigma -> types -> pinductive * types
+val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types
+val pf_reduce_to_atomic_ind : goal sigma -> types -> (inductive * EInstance.t) * types
val pf_compute : goal sigma -> constr -> constr
val pf_unfoldn : (occurrences * evaluable_global_reference) list
-> goal sigma -> constr -> constr
@@ -106,31 +107,31 @@ module New : sig
val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
- val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
+ val pf_concl : ('a, 'r) Proofview.Goal.t -> types
(** WRONG: To be avoided at all costs, it typechecks the term entirely but
forgets the universe constraints necessary to retypecheck it *)
- val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+ val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
(** This function does no type inference and expects an already well-typed term.
It recomputes its type in the fastest way possible (no conversion is ever involved) *)
- val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+ val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
(** This function entirely type-checks the term and computes its type
and the implied universe constraints. *)
- val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
- val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool
+ val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types
+ val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool
- val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
+ val pf_get_new_id : identifier -> ('a, 'r) Proofview.Goal.t -> identifier
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_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
- val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
+ val pf_get_hyp : identifier -> ('a, 'r) Proofview.Goal.t -> named_declaration
+ val pf_get_hyp_typ : identifier -> ('a, 'r) Proofview.Goal.t -> types
+ val pf_last_hyp : ('a, '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
+ val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> (inductive * EInstance.t) * types
val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 18:48:55 +0000