aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/eConstr.ml3
-rw-r--r--engine/eConstr.mli2
-rw-r--r--tactics/contradiction.ml11
-rw-r--r--tactics/eqdecide.ml27
-rw-r--r--tactics/equality.ml8
-rw-r--r--tactics/hipattern.ml2
-rw-r--r--tactics/hipattern.mli2
-rw-r--r--tactics/tactics.ml80
8 files changed, 79 insertions, 56 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c0485e4e7..5a05150d4 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -782,6 +782,9 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
Sigma.fresh_global ?loc ?rigid ?names env sigma reference in
Sigma.Sigma (of_constr t,sigma,p)
+let is_global sigma gr c =
+ Globnames.is_global gr (to_constr sigma c)
+
module Unsafe =
struct
let to_sorts = ESorts.unsafe_to_sorts
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9d705b4d5..9f45187cf 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -261,6 +261,8 @@ val fresh_global :
?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma
+val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
+
(** {5 Extra} *)
val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index fe44559ed..5e7090ded 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -19,10 +19,9 @@ module NamedDecl = Context.Named.Declaration
(* Absurd *)
-let mk_absurd_proof t =
- let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in
+let mk_absurd_proof coq_not t =
let id = Namegen.default_dependent_ident in
- mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]),
+ mkLambda (Names.Name id,mkApp(coq_not,[|t|]),
mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
let absurd c =
@@ -34,9 +33,11 @@ let absurd c =
let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
let t = j.Environ.utj_val in
let tac =
+ Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot ->
+ Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse ->
Tacticals.New.tclTHENLIST [
- elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()));
- Simple.apply (mk_absurd_proof t)
+ elim_type coqfalse;
+ Simple.apply (mk_absurd_proof coqnot t)
] in
Sigma.Unsafe.of_pair (tac, sigma)
end }
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bda25d7f0..48ce52f09 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -104,14 +104,9 @@ let solveNoteqBranch side =
(* Constructs the type {c1=c2}+{~c1=c2} *)
-let make_eq () =
-(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
-let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ())
-let build_coq_sumbool () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_sumbool ())
-
-let mkDecideEqGoal eqonleft op rectype c1 c2 =
- let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in
- let disequality = mkApp(build_coq_not (), [|equality|]) in
+let mkDecideEqGoal eqonleft (op,eq,neg) rectype c1 c2 =
+ let equality = mkApp(eq, [|rectype; c1; c2|]) in
+ let disequality = mkApp(neg, [|equality|]) in
if eqonleft then mkApp(op, [|equality; disequality |])
else mkApp(op, [|disequality; equality |])
@@ -121,13 +116,13 @@ let mkDecideEqGoal eqonleft op rectype c1 c2 =
let idx = Id.of_string "x"
let idy = Id.of_string "y"
-let mkGenDecideEqGoal rectype g =
+let mkGenDecideEqGoal rectype ops g =
let hypnames = pf_ids_of_hyps g in
let xname = next_ident_away idx hypnames
and yname = next_ident_away idy hypnames in
(mkNamedProd xname rectype
(mkNamedProd yname rectype
- (mkDecideEqGoal true (build_coq_sumbool ())
+ (mkDecideEqGoal true ops
rectype (mkVar xname) (mkVar yname))))
let rec rewrite_and_clear hyps = match hyps with
@@ -256,9 +251,9 @@ let decideGralEquality =
let decideEqualityGoal = tclTHEN intros decideGralEquality
-let decideEquality rectype =
+let decideEquality rectype ops =
Proofview.Goal.enter { enter = begin fun gl ->
- let decide = mkGenDecideEqGoal rectype gl in
+ let decide = mkGenDecideEqGoal rectype ops gl in
(tclTHENS (cut decide) [default_auto;decideEqualityGoal])
end }
@@ -266,11 +261,15 @@ let decideEquality rectype =
(* The tactic Compare *)
let compare c1 c2 =
+ pf_constr_of_global (build_coq_sumbool ()) >>= fun opc ->
+ pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc ->
+ pf_constr_of_global (build_coq_not ()) >>= fun notc ->
Proofview.Goal.enter { enter = begin fun gl ->
let rectype = pf_unsafe_type_of gl c1 in
- let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
+ let ops = (opc,eqc,notc) in
+ let decide = mkDecideEqGoal true ops rectype c1 c2 in
(tclTHENS (cut decide)
[(tclTHEN intro
(tclTHEN (onLastHyp simplest_case) clear_last));
- decideEquality rectype])
+ decideEquality rectype ops])
end }
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b48d60a4f..268daf6b6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1332,8 +1332,6 @@ let inject_if_homogenous_dependent_pair ty =
let sigma = Tacmach.New.project gl in
let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
(* fetch the informations of the pair *)
- let ceq = Universes.constr_of_global Coqlib.glob_eq in
- let ceq = EConstr.of_constr ceq in
let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
(* check whether the equality deals with dep pairs or not *)
@@ -1352,16 +1350,18 @@ let inject_if_homogenous_dependent_pair ty =
pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
- let inj2 = EConstr.of_constr @@ Universes.constr_of_global @@
- Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+ let inj2 = Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"]
+ "inj_pair2_eq_dec" in
let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
(* cut with the good equality and prove the requested goal *)
tclTHENLIST
[Proofview.tclEFFECTS eff;
intro;
onLastHyp (fun hyp ->
+ Tacticals.New.pf_constr_of_global Coqlib.glob_eq >>= fun ceq ->
tclTHENS (cut (mkApp (ceq,new_eq_args)))
[clear [destVar sigma hyp];
+ Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 ->
Proofview.V82.tactic (Tacmach.refine
(mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
])]
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index fd5eabe64..0d974be8b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -544,7 +544,7 @@ let match_eqdec sigma t =
false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in
match Id.Map.bindings subst with
| [(_,typ);(_,c1);(_,c2)] ->
- eqonleft, EConstr.of_constr (Universes.constr_of_global (Lazy.force op)), c1, c2, typ
+ eqonleft, Lazy.force op, c1, c2, typ
| _ -> anomaly (Pp.str "Unexpected pattern")
(* Patterns "~ ?" and "? -> False" *)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 82a3d47b5..9110830aa 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -142,7 +142,7 @@ val is_matching_sigma : evar_map -> constr -> bool
(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
[t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : evar_map -> constr -> bool * constr * constr * constr * constr
+val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
val dest_nf_eq : ('a, 'r) Proofview.Goal.t -> constr -> (constr * constr * constr)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e8cb4e63..3efaf0cc6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3519,27 +3519,32 @@ let error_ind_scheme s =
let s = if not (String.is_empty s) then s^" " else s in
user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
-let glob c = EConstr.of_constr (Universes.constr_of_global c)
+let glob sigma gr =
+ let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+ in Sigma.to_evar_map sigma, c
-let coq_eq = lazy (glob (Coqlib.build_coq_eq ()))
-let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ()))
+let coq_eq sigma = glob sigma (Coqlib.build_coq_eq ())
+let coq_eq_refl sigma = glob sigma (Coqlib.build_coq_eq_refl ())
-let coq_heq = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq"))
-let coq_heq_refl = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl"))
+let coq_heq_ref = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")
+let coq_heq sigma = glob sigma (Lazy.force coq_heq_ref)
+let coq_heq_refl sigma = glob sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
-let mkEq t x y =
- mkApp (Lazy.force coq_eq, [| t; x; y |])
+let mkEq sigma t x y =
+ let sigma, eq = coq_eq sigma in
+ sigma, mkApp (eq, [| t; x; y |])
-let mkRefl t x =
- mkApp (Lazy.force coq_eq_refl, [| t; x |])
+let mkRefl sigma t x =
+ let sigma, refl = coq_eq_refl sigma in
+ sigma, mkApp (refl, [| t; x |])
-let mkHEq t x u y =
- mkApp (Lazy.force coq_heq,
- [| t; x; u; y |])
+let mkHEq sigma t x u y =
+ let sigma, c = coq_heq sigma in
+ sigma, mkApp (c,[| t; x; u; y |])
-let mkHRefl t x =
- mkApp (Lazy.force coq_heq_refl,
- [| t; x |])
+let mkHRefl sigma t x =
+ let sigma, c = coq_heq_refl sigma in
+ sigma, mkApp (c, [| t; x |])
let lift_togethern n l =
let l', _ =
@@ -3577,23 +3582,30 @@ let decompose_indapp sigma f args =
mkApp (f, pars), args
| _ -> f, args
-let mk_term_eq env sigma ty t ty' t' =
+let mk_term_eq homogeneous env sigma ty t ty' t' =
let sigma = Sigma.to_evar_map sigma in
- if Reductionops.is_conv env sigma ty ty' then
- mkEq ty t t', mkRefl ty' t'
+ if homogeneous then
+ let sigma, eq = mkEq sigma ty t t' in
+ let sigma, refl = mkRefl sigma ty' t' in
+ Sigma.Unsafe.of_evar_map sigma, (eq, refl)
else
- mkHEq ty t ty' t', mkHRefl ty' t'
+ let sigma, heq = mkHEq sigma ty t ty' t' in
+ let sigma, hrefl = mkHRefl sigma ty' t' in
+ Sigma.Unsafe.of_evar_map sigma, (heq, hrefl)
let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
let open Context.Rel.Declaration in
Refine.refine { run = begin fun sigma ->
let eqslen = List.length eqs in
(* Abstract by the "generalized" hypothesis equality proof if necessary. *)
- let abshypeq, abshypt =
+ let sigma, abshypeq, abshypt =
if dep then
- let eq, refl = mk_term_eq (push_rel_context ctx env) sigma (lift 1 c) (mkRel 1) typ (mkVar id) in
- mkProd (Anonymous, eq, lift 1 concl), [| refl |]
- else concl, [||]
+ let ty = lift 1 c in
+ let homogeneous = Reductionops.is_conv env (Sigma.to_evar_map sigma) ty typ in
+ let sigma, (eq, refl) =
+ mk_term_eq homogeneous (push_rel_context ctx env) sigma ty (mkRel 1) typ (mkVar id) in
+ sigma, mkProd (Anonymous, eq, lift 1 concl), [| refl |]
+ else sigma, concl, [||]
in
(* Abstract by equalities *)
let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
@@ -3699,9 +3711,13 @@ let abstract_args gl generalize_vars dep id defined f args =
let liftarg = lift (List.length ctx) arg in
let eq, refl =
if leq then
- mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl (lift (-lenctx) ty) arg
+ let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in
+ let sigma', refl = mkRefl sigma' (lift (-lenctx) ty) arg in
+ sigma := sigma'; eq, refl
else
- mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
+ let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in
+ let sigma', refl = mkHRefl sigma' argty arg in
+ sigma := sigma'; eq, refl
in
let eqs = eq :: lift_list eqs in
let refls = refl :: refls in
@@ -3801,17 +3817,19 @@ let specialize_eqs id gl =
match EConstr.kind !evars ty with
| Prod (na, t, b) ->
(match EConstr.kind !evars t with
- | App (eq, [| eqty; x; y |]) when EConstr.eq_constr !evars (Lazy.force coq_eq) eq ->
+ | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars (Lazy.force coq_eq_ref) eq ->
let c = if noccur_between !evars 1 (List.length ctx) x then y else x in
- let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in
- let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in
+ let pt = mkApp (eq, [| eqty; c; c |]) in
+ let ind = destInd !evars eq in
+ let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in
if unif (push_rel_context ctx env) evars pt t then
aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
else acc, in_eqs, ctx, ty
- | App (heq, [| eqty; x; eqty'; y |]) when EConstr.eq_constr !evars heq (Lazy.force coq_heq) ->
+ | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq ->
let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in
- let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in
- let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in
+ let pt = mkApp (heq, [| eqt; c; eqt; c |]) in
+ let ind = destInd !evars heq in
+ let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in
if unif (push_rel_context ctx env) evars pt t then
aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
else acc, in_eqs, ctx, ty
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 13:25:39 +0000