diff options
Diffstat (limited to 'plugins')
38 files changed, 108 insertions, 44 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 1ce1660b32..0f5b806644 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -255,7 +255,7 @@ let app_global_with_holes f args n = Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - Refine.refine begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let t = Tacmach.New.pf_get_type_of gl fc in let t = Termops.prod_applist sigma t (Array.to_list args) in let ans = mkApp (fc, args) in diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v index 294d61023b..d08a81da64 100644 --- a/plugins/extraction/ExtrHaskellBasic.v +++ b/plugins/extraction/ExtrHaskellBasic.v @@ -1,5 +1,7 @@ (** Extraction to Haskell : use of basic Haskell types *) +Require Coq.extraction.Extraction. + Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. Extract Inductive unit => "()" [ "()" ]. diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v index e94e7d42bd..267322d9ed 100644 --- a/plugins/extraction/ExtrHaskellNatInt.v +++ b/plugins/extraction/ExtrHaskellNatInt.v @@ -1,5 +1,7 @@ (** Extraction of [nat] into Haskell's [Int] *) +Require Coq.extraction.Extraction. + Require Import Arith. Require Import ExtrHaskellNatNum. diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/plugins/extraction/ExtrHaskellNatInteger.v index 038f0ed817..4c5c71f58a 100644 --- a/plugins/extraction/ExtrHaskellNatInteger.v +++ b/plugins/extraction/ExtrHaskellNatInteger.v @@ -1,5 +1,7 @@ (** Extraction of [nat] into Haskell's [Integer] *) +Require Coq.extraction.Extraction. + Require Import Arith. Require Import ExtrHaskellNatNum. diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v index 244eb85fc2..fabe9a4c67 100644 --- a/plugins/extraction/ExtrHaskellNatNum.v +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -6,6 +6,8 @@ * implements [Num]. *) +Require Coq.extraction.Extraction. + Require Import Arith. Require Import EqNat. diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v index 3558f4f254..ac1f6f9130 100644 --- a/plugins/extraction/ExtrHaskellString.v +++ b/plugins/extraction/ExtrHaskellString.v @@ -2,6 +2,8 @@ * Special handling of ascii and strings for extraction to Haskell. *) +Require Coq.extraction.Extraction. + Require Import Ascii. Require Import String. diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v index 66690851a7..0345ffc4e8 100644 --- a/plugins/extraction/ExtrHaskellZInt.v +++ b/plugins/extraction/ExtrHaskellZInt.v @@ -1,5 +1,7 @@ (** Extraction of [Z] into Haskell's [Int] *) +Require Coq.extraction.Extraction. + Require Import ZArith. Require Import ExtrHaskellZNum. diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/plugins/extraction/ExtrHaskellZInteger.v index f192f16ee8..f7f9e2f80d 100644 --- a/plugins/extraction/ExtrHaskellZInteger.v +++ b/plugins/extraction/ExtrHaskellZInteger.v @@ -1,5 +1,7 @@ (** Extraction of [Z] into Haskell's [Integer] *) +Require Coq.extraction.Extraction. + Require Import ZArith. Require Import ExtrHaskellZNum. diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v index cbbfda75e5..4141bd203f 100644 --- a/plugins/extraction/ExtrHaskellZNum.v +++ b/plugins/extraction/ExtrHaskellZNum.v @@ -6,6 +6,8 @@ * implements [Num]. *) +Require Coq.extraction.Extraction. + Require Import ZArith. Require Import EqNat. diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index d9b000c2af..dfdc498638 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Coq.extraction.Extraction. + (** Extraction to Ocaml : use of basic Ocaml types *) Extract Inductive bool => bool [ true false ]. diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v index c42938c8ec..78ee460856 100644 --- a/plugins/extraction/ExtrOcamlBigIntConv.v +++ b/plugins/extraction/ExtrOcamlBigIntConv.v @@ -13,6 +13,8 @@ simplifies the use of [Big_int] (it can be found in the sources of Coq). *) +Require Coq.extraction.Extraction. + Require Import Arith ZArith. Parameter bigint : Type. diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v index 515fa52dfa..fcfea352a7 100644 --- a/plugins/extraction/ExtrOcamlIntConv.v +++ b/plugins/extraction/ExtrOcamlIntConv.v @@ -10,6 +10,8 @@ Nota: no check that [int] values aren't generating overflows *) +Require Coq.extraction.Extraction. + Require Import Arith ZArith. Parameter int : Type. diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index 3149e70298..e0837be621 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -8,6 +8,8 @@ (** Extraction of [nat] into Ocaml's [big_int] *) +Require Coq.extraction.Extraction. + Require Import Arith Even Div2 EqNat Euclid. Require Import ExtrOcamlBasic. diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 7c607f7ae6..80da72d43f 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -8,6 +8,8 @@ (** Extraction of [nat] into Ocaml's [int] *) +Require Coq.extraction.Extraction. + Require Import Arith Even Div2 EqNat Euclid. Require Import ExtrOcamlBasic. diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index 6af591eed3..64ca6c85d0 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -8,6 +8,8 @@ (* Extraction to Ocaml : special handling of ascii and strings *) +Require Coq.extraction.Extraction. + Require Import Ascii String. Extract Inductive ascii => char diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index c9e8eac0c5..66f188c84e 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -8,6 +8,8 @@ (** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *) +Require Coq.extraction.Extraction. + Require Import ZArith NArith. Require Import ExtrOcamlBasic. diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index 4d33174b35..c93cfb9d46 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -8,6 +8,8 @@ (** Extraction of [positive], [N] and [Z] into Ocaml's [int] *) +Require Coq.extraction.Extraction. + Require Import ZArith NArith. Require Import ExtrOcamlBasic. diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v new file mode 100644 index 0000000000..ab1416b1d6 --- /dev/null +++ b/plugins/extraction/Extraction.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Declare ML Module "extraction_plugin".
\ No newline at end of file diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v new file mode 100644 index 0000000000..e40aea7764 --- /dev/null +++ b/plugins/funind/FunInd.v @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Coq.extraction.Extraction. +Declare ML Module "recdef_plugin". diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index e4433247b4..64f43b8335 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Export Coq.funind.FunInd. Require Import PeanoNat. - Require Compare_dec. Require Wf_nat. diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 70245a8b1e..8ffd15f9fb 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -371,12 +371,12 @@ let generate_functional_principle (evd: Evd.evar_map ref) begin begin try - let id = Pfedit.get_current_proof_name () in + let id = Proof_global.get_current_proof_name () in let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () + then Proof_global.discard_current () else () else () with e when CErrors.noncritical e -> () @@ -524,12 +524,12 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con begin begin try - let id = Pfedit.get_current_proof_name () in + let id = Proof_global.get_current_proof_name () in let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () + then Proof_global.discard_current () else () else () with e when CErrors.noncritical e -> () diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index a7481370a3..726a8203d7 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -722,7 +722,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect (* we first (pseudo) understand [rt] and get back the computed evar_map *) (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) - let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Pretyping.empty_lvar expected_type rt in + let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in let ctx, f = Evarutil.nf_evars_and_universes ctx in (* then we map [rt] to replace the implicit holes by their values *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7558ac7ac2..6fe6888f3d 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -161,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook = let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in - if with_clean then Pfedit.delete_current_proof (); + if with_clean then Proof_global.discard_current (); CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id @@ -173,7 +173,7 @@ let cook_proof _ = let get_proof_clean do_reduce = let result = cook_proof do_reduce in - Pfedit.delete_current_proof (); + Proof_global.discard_current (); result let with_full_print f a = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 20abde82f2..3cd20a9507 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1295,7 +1295,7 @@ let is_opaque_constant c = let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) - let current_proof_name = get_current_proof_name () in + let current_proof_name = Proof_global.get_current_proof_name () in let name = match goal_name with | Some s -> s | None -> diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index a299e11f8a..7ecfa57f6d 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -28,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma = let filtered = Evd.evar_filtered_env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in let lvar = { - Pretyping.ltac_constrs = constrvars; + Glob_term.ltac_constrs = constrvars; ltac_uconstrs = Names.Id.Map.empty; ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 18d7b818cd..7259faecd0 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -365,7 +365,7 @@ let refine_tac ist simple with_classes c = let update = begin fun sigma -> c env sigma end in - let refine = Refine.refine ~unsafe:true update in + let refine = Refine.refine ~typecheck:false update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index a971fc79f6..804f734504 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -139,14 +139,16 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with end | _ -> ElimOnConstr clbind +let mkNumeral n = Numeral (string_of_int (abs n), 0<=n) + let mkTacCase with_evar = function | [(clear,ElimOnConstr cl),(None,None),None],None -> TacCase (with_evar,(clear,cl)) (* Reinterpret numbers as a notation for terms *) | [(clear,ElimOnAnonHyp n),(None,None),None],None -> TacCase (with_evar, - (clear,(CAst.make @@ CPrim (Numeral (Bigint.of_int n)), - NoBindings))) + (clear,(CAst.make @@ CPrim (mkNumeral n), + NoBindings))) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3927ca7ce1..fad181c897 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1539,7 +1539,7 @@ let assert_replacing id newt tac = | 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 begin fun sigma -> + Refine.refine ~typecheck:true begin fun sigma -> let (sigma, ev) = Evarutil.new_evar env' sigma concl in let (sigma, ev') = Evarutil.new_evar env sigma newt in let map d = @@ -1573,7 +1573,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = match clause, prf with | Some id, Some p -> let tac = tclTHENLIST [ - Refine.refine ~unsafe:false (fun h -> (h,p)); + Refine.refine ~typecheck:true (fun h -> (h,p)); Proofview.Unsafe.tclNEWGOALS gls; ] in Proofview.Unsafe.tclEVARS undef <*> @@ -1590,7 +1590,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let (sigma, ev) = Evarutil.new_evar env sigma newt in (sigma, mkApp (p, [| ev |])) end in - Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls + Refine.refine ~typecheck:true make <*> Proofview.Unsafe.tclNEWGOALS gls end | None, None -> Proofview.Unsafe.tclEVARS undef <*> diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9b6ac8a9ae..67893bd11e 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -386,7 +386,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map + | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map type ltac_trace = ltac_call_kind Loc.located list diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 9d8094205b..0cd3ee2f9c 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -22,7 +22,6 @@ open Nameops open Libnames open Globnames open Nametab -open Pfedit open Refiner open Tacmach.New open Tactic_debug @@ -605,10 +604,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = let { closure = constrvars ; term } = interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in let vars = { - Pretyping.ltac_constrs = constrvars.typed; - Pretyping.ltac_uconstrs = constrvars.untyped; - Pretyping.ltac_idents = constrvars.idents; - Pretyping.ltac_genargs = ist.lfun; + Glob_term.ltac_constrs = constrvars.typed; + Glob_term.ltac_uconstrs = constrvars.untyped; + Glob_term.ltac_idents = constrvars.idents; + Glob_term.ltac_genargs = ist.lfun; } in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do @@ -629,7 +628,7 @@ let interp_gen kind ist pattern_mode flags env sigma c = let constr_flags () = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = solve_by_implicit_tactic (); + use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = true; expand_evars = true } @@ -644,14 +643,14 @@ let interp_type = interp_constr_gen IsType let open_constr_use_classes_flags () = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = solve_by_implicit_tactic (); + use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } let open_constr_no_classes_flags () = { use_typeclasses = false; solve_unification_constraints = true; - use_hook = solve_by_implicit_tactic (); + use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index b909c930db..53dc800231 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -364,7 +364,7 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.tag te))) - | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) -> + | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 5eacb1a95e..2a8ed72387 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -66,7 +66,7 @@ let negation_unfolding = ref true (* Whether inner iff are unfolded *) let iff_unfolding = ref false -let unfold_iff () = !iff_unfolding || Flags.version_less_or_equal Flags.V8_2 +let unfold_iff () = !iff_unfolding open Goptions let _ = @@ -79,7 +79,7 @@ let _ = let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "unfolding of iff in intuition"; optkey = ["Intuition";"Iff";"Unfolding"]; optread = (fun () -> !iff_unfolding); diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 2451aeada7..95f135c8f0 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -14,6 +14,7 @@ (* Used to generate micromega.ml *) +Require Extraction. Require Import ZMicromega. Require Import QMicromega. Require Import RMicromega. @@ -48,7 +49,10 @@ Extract Constant Rmult => "( * )". Extract Constant Ropp => "fun x -> - x". Extract Constant Rinv => "fun x -> 1 / x". -Extraction "plugins/micromega/generated_micromega.ml" +(** We now extract to stdout, see comment in Makefile.build *) + +(*Extraction "plugins/micromega/micromega.ml" *) +Recursive Extraction List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 6c0e2d776d..2780be4aaa 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -48,10 +48,13 @@ Ltac zify_unop_var_or_term t thm a := (remember a as za; zify_unop_core t thm za). Ltac zify_unop t thm a := - (* if a is a scalar, we can simply reduce the unop *) + (* If a is a scalar, we can simply reduce the unop. *) + (* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *) let isz := isZcst a in match isz with - | true => simpl (t a) in * + | true => + let u := eval compute in (t a) in + change (t a) with u in * | _ => zify_unop_var_or_term t thm a end. @@ -165,14 +168,16 @@ Ltac zify_nat_op := rewrite (Nat2Z.inj_mul a b) in * (* O -> Z0 *) - | H : context [ Z.of_nat O ] |- _ => simpl (Z.of_nat O) in H - | |- context [ Z.of_nat O ] => simpl (Z.of_nat O) + | H : context [ Z.of_nat O ] |- _ => change (Z.of_nat O) with Z0 in H + | |- context [ Z.of_nat O ] => change (Z.of_nat O) with Z0 (* S -> number or Z.succ *) | H : context [ Z.of_nat (S ?a) ] |- _ => let isnat := isnatcst a in match isnat with - | true => simpl (Z.of_nat (S a)) in H + | true => + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t in H | _ => rewrite (Nat2Z.inj_succ a) in H | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), hide [Z.of_nat (S a)] in this one hypothesis *) @@ -181,7 +186,9 @@ Ltac zify_nat_op := | |- context [ Z.of_nat (S ?a) ] => let isnat := isnatcst a in match isnat with - | true => simpl (Z.of_nat (S a)) + | true => + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t | _ => rewrite (Nat2Z.inj_succ a) | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), hide [Z.of_nat (S a)] in the goal *) @@ -264,8 +271,8 @@ Ltac zify_positive_op := | |- context [ Zpos (Pos.max ?a ?b) ] => rewrite (Pos2Z.inj_max a b) (* Pos.sub -> Z.max 1 (Z.sub ... ...) *) - | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub a b) in H - | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub a b) + | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub_max a b) in H + | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub_max a b) (* Pos.succ -> Z.succ *) | H : context [ Zpos (Pos.succ ?a) ] |- _ => rewrite (Pos2Z.inj_succ a) in H diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 9cb94b68df..440a10bfb9 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -652,7 +652,7 @@ let clever_rewrite_base_poly typ p result theorem = let full = pf_concl gl in let env = pf_env gl in let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in - Refine.refine begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let t = applist (mkLambda @@ -688,7 +688,7 @@ let clever_rewrite_gen_nat p result (t,args) = (** Solve using the term the term [t _] *) let refine_app gl t = let open Tacmach.New in - Refine.refine begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let env = pf_env gl in let ht = match EConstr.kind sigma (pf_get_type_of gl t) with | Prod (_, t, _) -> t diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d389f70859..490ded9d4d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -226,8 +226,8 @@ let isAppInd gl c = let interp_refine ist gl rc = let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in - let vars = { Pretyping.empty_lvar with - Pretyping.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun + let vars = { Glob_ops.empty_lvar with + Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun } in let kind = Pretyping.OfType (pf_concl gl) in let flags = { diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 4a9dddd2ba..7ae9e38248 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -95,7 +95,7 @@ let ssrmkabs id gl = end in Proofview.V82.of_tactic (Proofview.tclTHEN - (Tactics.New.refine step) + (Tactics.New.refine ~typecheck:false step) (Proofview.tclFOCUS 1 3 Proofview.shelve)) gl let ssrmkabstac ids = diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 3ea8c24314..09917339a7 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -346,7 +346,8 @@ let interp_index ist gl idx = | Some c -> let rc = Detyping.detype false [] (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc with - | _, Constrexpr.Numeral bigi -> int_of_string (Bigint.to_string bigi) + | _, Constrexpr.Numeral (s,b) -> + let n = int_of_string s in if b then n else -n | _ -> raise Not_found end | None -> raise Not_found |