aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/ltac/extratactics.ml428
-rw-r--r--plugins/omega/coq_omega.ml54
-rw-r--r--plugins/romega/const_omega.ml12
-rw-r--r--plugins/setoid_ring/ArithRing.v19
5 files changed, 51 insertions, 64 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 47e8123191..4ae875cd70 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -302,7 +302,7 @@ let rec extract_type env db j c args =
if Projection.unfolded p then Tunknown
else extract_type env db j (mkProj (Projection.unfold p, t)) args
| Case _ | Fix _ | CoFix _ -> Tunknown
- | _ -> assert false
+ | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false
(*s Auxiliary function dealing with type application.
Precondition: [r] is a type scheme represented by the signature [s],
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d6cfa3cf9a..790a9e4352 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -873,34 +873,12 @@ TACTIC EXTEND is_evar
]
END
-let has_evar sigma c =
-let rec has_evar x =
- match EConstr.kind sigma x with
- | Evar _ -> true
- | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ ->
- false
- | Cast (t1, _, t2) | Prod (_, t1, t2) | Lambda (_, t1, t2) ->
- has_evar t1 || has_evar t2
- | LetIn (_, t1, t2, t3) ->
- has_evar t1 || has_evar t2 || has_evar t3
- | App (t1, ts) ->
- has_evar t1 || has_evar_array ts
- | Case (_, t1, t2, ts) ->
- has_evar t1 || has_evar t2 || has_evar_array ts
- | Fix ((_, tr)) | CoFix ((_, tr)) ->
- has_evar_prec tr
- | Proj (p, c) -> has_evar c
-and has_evar_array x =
- Array.exists has_evar x
-and has_evar_prec (_, ts1, ts2) =
- Array.exists has_evar ts1 || Array.exists has_evar ts2
-in
-has_evar c
-
TACTIC EXTEND has_evar
| [ "has_evar" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- if has_evar sigma x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars")
+ if Evarutil.has_undefined_evars sigma x
+ then Proofview.tclUNIT ()
+ else Tacticals.New.tclFAIL 0 (str "No evars")
]
END
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ff69ddefb8..8692842468 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -466,12 +466,14 @@ let destructurate_prop sigma t =
| Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal")
| _ -> Kufo
-let destructurate_type sigma t =
- let eq_constr c1 c2 = eq_constr sigma c1 c2 in
- let c, args = decompose_app sigma t in
+let nf = Tacred.simpl
+
+let destructurate_type env sigma t =
+ let is_conv = Reductionops.is_conv env sigma in
+ let c, args = decompose_app sigma (nf env sigma t) in
match EConstr.kind sigma c, args with
- | _, [] when eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args)
- | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args)
+ | _, [] when is_conv c (Lazy.force coq_Z) -> Kapp (Z,args)
+ | _, [] when is_conv c (Lazy.force coq_nat) -> Kapp (Nat,args)
| _ -> Kufo
let destructurate_term sigma t =
@@ -1459,17 +1461,13 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
else
(tactic,defs)
-let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
-
-let destructure_omega gl tac_def (id,c) =
- let open Tacmach.New in
- let sigma = project gl in
+let destructure_omega env sigma tac_def (id,c) =
if String.equal (atompart_of_id id) "State" then
tac_def
else
try match destructurate_prop sigma c with
| Kapp(Eq,[typ;t1;t2])
- when begin match destructurate_type sigma (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end ->
+ when begin match destructurate_type env sigma typ with Kapp(Z,[]) -> true | _ -> false end ->
let t = mk_plus t1 (mk_inv t2) in
normalize_equation sigma
id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
@@ -1507,7 +1505,7 @@ let coq_omega =
Proofview.Goal.enter begin fun gl ->
clear_constr_tables ();
let hyps_types = Tacmach.New.pf_hyps_types gl in
- let destructure_omega = destructure_omega gl in
+ let destructure_omega = Tacmach.New.pf_apply destructure_omega gl in
let tactic_normalisation, system =
List.fold_left destructure_omega ([],[]) hyps_types in
let prelude,sys =
@@ -1727,27 +1725,26 @@ let not_binop = function
exception Undecidable
-let rec decidability gl t =
- let open Tacmach.New in
- match destructurate_prop (project gl) t with
+let rec decidability env sigma t =
+ match destructurate_prop sigma t with
| Kapp(Or,[t1;t2]) ->
mkApp (Lazy.force coq_dec_or, [| t1; t2;
- decidability gl t1; decidability gl t2 |])
+ decidability env sigma t1; decidability env sigma t2 |])
| Kapp(And,[t1;t2]) ->
mkApp (Lazy.force coq_dec_and, [| t1; t2;
- decidability gl t1; decidability gl t2 |])
+ decidability env sigma t1; decidability env sigma t2 |])
| Kapp(Iff,[t1;t2]) ->
mkApp (Lazy.force coq_dec_iff, [| t1; t2;
- decidability gl t1; decidability gl t2 |])
+ decidability env sigma t1; decidability env sigma t2 |])
| Kimp(t1,t2) ->
(* This is the only situation where it's not obvious that [t]
is in Prop. The recursive call on [t2] will ensure that. *)
mkApp (Lazy.force coq_dec_imp,
- [| t1; t2; decidability gl t1; decidability gl t2 |])
+ [| t1; t2; decidability env sigma t1; decidability env sigma t2 |])
| Kapp(Not,[t1]) ->
- mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |])
+ mkApp (Lazy.force coq_dec_not, [| t1; decidability env sigma t1 |])
| Kapp(Eq,[typ;t1;t2]) ->
- begin match destructurate_type (project gl) (pf_nf gl typ) with
+ begin match destructurate_type env sigma typ with
| Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
| Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
| _ -> raise Undecidable
@@ -1784,15 +1781,16 @@ let onClearedName2 id tac =
let destructure_hyps =
Proofview.Goal.enter begin fun gl ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
- let decidability = decidability gl in
- let pf_nf = pf_nf gl in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let decidability = decidability env sigma in
let rec loop = function
| [] -> (tclTHEN nat_inject coq_omega)
| LocalDef (i,body,typ) :: lit when !letin_flag ->
Proofview.tclEVARMAP >>= fun sigma ->
begin
try
- match destructurate_type sigma (pf_nf typ) with
+ match destructurate_type env sigma typ with
| Kapp(Nat,_) | Kapp(Z,_) ->
let hid = fresh_id Id.Set.empty (add_suffix i "_eqn") gl in
let hty = mk_gen_eq typ (mkVar i) body in
@@ -1895,7 +1893,7 @@ let destructure_hyps =
with Not_found -> loop lit)
| Kapp(Eq,[typ;t1;t2]) ->
if !old_style_flag then begin
- match destructurate_type sigma (pf_nf typ) with
+ match destructurate_type env sigma typ with
| Kapp(Nat,_) ->
tclTHENLIST [
(simplest_elim
@@ -1912,7 +1910,7 @@ let destructure_hyps =
]
| _ -> loop lit
end else begin
- match destructurate_type sigma (pf_nf typ) with
+ match destructurate_type env sigma typ with
| Kapp(Nat,_) ->
(tclTHEN
(convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
@@ -1940,7 +1938,9 @@ let destructure_hyps =
let destructure_goal =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
- let decidability = decidability gl in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let decidability = decidability env sigma in
let rec loop t =
Proofview.tclEVARMAP >>= fun sigma ->
let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 32a1c07b27..337510ef1f 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -197,6 +197,7 @@ let parse_logic_rel c = match destructurate c with
(* Binary numbers *)
+let coq_Z = lazy (bin_constant "Z")
let coq_xH = lazy (bin_constant "xH")
let coq_xO = lazy (bin_constant "xO")
let coq_xI = lazy (bin_constant "xI")
@@ -237,7 +238,7 @@ end
module Z : Int = struct
-let typ = lazy (bin_constant "Z")
+let typ = coq_Z
let plus = lazy (z_constant "Z.add")
let mult = lazy (z_constant "Z.mul")
let opp = lazy (z_constant "Z.opp")
@@ -285,14 +286,9 @@ let parse_term t =
(match recognize_Z t with Some t -> Tnum t | None -> Tother)
| _ -> Tother
-let pf_nf gl c =
- EConstr.Unsafe.to_constr
- (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c))
-
let is_int_typ gl t =
- match destructurate (pf_nf gl t) with
- | Kapp("Z",[]) -> true
- | _ -> false
+ Tacmach.New.pf_apply Reductionops.is_conv gl
+ (EConstr.of_constr t) (EConstr.of_constr (Lazy.force coq_Z))
let parse_rel gl t =
match destructurate t with
diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 447acb9057..8e4d8b0d34 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -41,9 +41,12 @@ Ltac Ss_to_add f acc :=
| _ => constr:((acc + f)%nat)
end.
+(* For internal use only *)
+Local Definition protected_to_nat := N.to_nat.
+
Ltac natprering :=
match goal with
- |- context C [S ?p] =>
+ |- context C [S ?p] =>
match p with
O => fail 1 (* avoid replacing 1 with 1+0 ! *)
| p => match isnatcst p with
@@ -52,9 +55,19 @@ Ltac natprering :=
fold v; natprering
end
end
- | _ => idtac
+ | _ => change N.to_nat with protected_to_nat
+ end.
+
+Ltac natpostring :=
+ match goal with
+ | |- context [N.to_nat ?x] =>
+ let v := eval cbv in (N.to_nat x) in
+ change (N.to_nat x) with v;
+ natpostring
+ | _ => change protected_to_nat with N.to_nat
end.
Add Ring natr : natSRth
- (morphism nat_morph_N, constants [natcst], preprocess [natprering]).
+ (morphism nat_morph_N, constants [natcst],
+ preprocess [natprering], postprocess [natpostring]).
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 04:46:12 +0000