diff options
Diffstat (limited to 'plugins')
72 files changed, 289 insertions, 229 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 5c7cad7ff5..39fb8feeb8 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -270,7 +270,7 @@ type state = mutable rew_depth:int; mutable changed:bool; by_type: Int.Set.t Typehash.t; - mutable gls:Proof_type.goal Evd.sigma} + mutable gls:Goal.goal Evd.sigma} let dummy_node = { diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 505029992a..51e2301fe6 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -129,7 +129,7 @@ val axioms : forest -> (term * term) Constrhash.t val epsilons : forest -> pa_constructor list -val empty : int -> Proof_type.goal Evd.sigma -> state +val empty : int -> Goal.goal Evd.sigma -> state val add_term : state -> term -> int 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_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ef894b2395..ba46f78aa8 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -10,7 +10,6 @@ open Names open Pp open Tacmach open Termops -open Proof_type open Tacticals open Tactics open Indfun_common @@ -106,7 +105,7 @@ let make_refl_eq constructor type_of_t t = type pte_info = { - proving_tac : (Id.t list -> Proof_type.tactic); + proving_tac : (Id.t list -> Tacmach.tactic); is_valid : constr -> bool } diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 5bb288678d..d03fc475e0 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -4,7 +4,7 @@ open Names val prove_princ_for_struct : Evd.evar_map ref -> bool -> - int -> Constant.t array -> EConstr.constr array -> int -> Proof_type.tactic + int -> Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic val prove_principle_for_gen : @@ -14,7 +14,7 @@ val prove_principle_for_gen : int -> (* the number of recursive argument *) EConstr.types -> (* the type of the recursive argument *) EConstr.constr -> (* the wf relation used to prove the function *) - Proof_type.tactic + Tacmach.tactic (* val is_pte : rel_declaration -> bool *) 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/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index bb2b2d9186..e70ef23656 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -28,7 +28,7 @@ val generate_functional_principle : (* The tactic to use to make the proof w.r the number of params *) - (EConstr.constr array -> int -> Proof_type.tactic) -> + (EConstr.constr array -> int -> Tacmach.tactic) -> unit val compute_new_princ_type_from_rel : constr array -> Sorts.t array -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 0e2ca49000..db2af2be53 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1459,7 +1459,9 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print + (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1470,7 +1472,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1485,7 +1487,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ CErrors.print reraise in 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.ml b/plugins/funind/indfun.ml index d12aa7f425..2c5dae1cde 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -343,7 +343,7 @@ let error_error names e = let generate_principle (evd:Evd.evar_map ref) pconstants on_error is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> - Proof_type.tactic) : unit = + Tacmach.tactic) : unit = let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in @@ -446,7 +446,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation - (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Proof_type.tactic = + (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic = Functional_principles_proofs.prove_principle_for_gen (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation @@ -576,50 +576,44 @@ let map_option f = function | Some v -> Some (f v) open Constrexpr -open Topconstr -let make_assoc assoc l1 l2 = - let fold assoc a b = match a, b with - | (_, Name na), (_, Name id) -> Id.Map.add na id assoc - | _, _ -> assoc - in - List.fold_left2 fold assoc l1 l2 - -let rec rebuild_bl (aux,assoc) bl typ = - match bl,typ with - | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) - | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> - rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } -> - rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) +let rec rebuild_bl aux bl typ = + match bl,typ with + | [], _ -> List.rev aux,typ + | (CLocalAssum(nal,bk,_))::bl',typ -> + rebuild_nal aux bk bl' nal typ + | (CLocalDef(na,_,_))::bl',{ CAst.v = CLetIn(_,nat,ty,typ') } -> + rebuild_bl (Constrexpr.CLocalDef(na,nat,ty)::aux) bl' typ' | _ -> assert false - and rebuild_nal (aux,assoc) bk bl' nal lnal typ = - match nal, typ.CAst.v with - | [], _ -> rebuild_bl (aux,assoc) bl' typ - | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ - | _,CProdN((nal',bk',nal't)::rest,typ') -> - let lnal' = List.length nal' in - if lnal' >= lnal - then - let old_nal',new_nal' = List.chop lnal nal' in - let nassoc = make_assoc assoc old_nal' nal in - let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in - rebuild_bl ((assum :: aux), nassoc) bl' - (if List.is_empty new_nal' && List.is_empty rest - then typ' - else CAst.make @@ if List.is_empty new_nal' - then CProdN(rest,typ') - else CProdN(((new_nal',bk',nal't)::rest),typ')) - else - let captured_nal,non_captured_nal = List.chop lnal' nal in - let nassoc = make_assoc assoc nal' captured_nal in - let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in - rebuild_nal ((assum :: aux), nassoc) - bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ')) - | _ -> assert false - -let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ +and rebuild_nal aux bk bl' nal typ = + match nal,typ with + | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ + | [], _ -> rebuild_bl aux bl' typ + | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } -> + if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') + then + let assum = CLocalAssum([na],bk,nal't) in + let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + rebuild_nal + (assum::aux) + bk + bl' + nal + (CAst.make @@ CProdN(new_rest,typ')) + else + let assum = CLocalAssum([na'],bk,nal't) in + let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + rebuild_nal + (assum::aux) + bk + bl' + (na::nal) + (CAst.make @@ CProdN(new_rest,typ')) + | _ -> + assert false + +let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in @@ -629,7 +623,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> - let new_bl',new_ret_type,_ = rebuild_bl ([],Id.Map.empty) bl fix_typ in + let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixpoint_exprl constr_expr_typel diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 33420d8132..fc7da6a338 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -16,7 +16,7 @@ val functional_induction : EConstr.constr -> (EConstr.constr * EConstr.constr bindings) option -> Tacexpr.or_and_intro_pattern option -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val make_graph : Globnames.global_reference -> unit 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/indfun_common.mli b/plugins/funind/indfun_common.mli index 6b40c91713..f7a9cedd73 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -105,7 +105,7 @@ exception ToShow of exn val is_strict_tcc : unit -> bool -val h_intros: Names.Id.t list -> Proof_type.tactic +val h_intros: Names.Id.t list -> Tacmach.tactic val h_id : Names.Id.t val hrec_id : Names.Id.t val acc_inv_id : EConstr.constr Util.delayed @@ -114,7 +114,7 @@ val well_founded_ltof : EConstr.constr Util.delayed val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference -val list_rewrite : bool -> (EConstr.constr*bool) list -> Proof_type.tactic +val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ebdb490e37..94ef2590c8 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -218,7 +218,7 @@ let rec generate_fresh_id x avoid i = \end{enumerate} *) -let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Proof_type.tactic = +let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = fun g -> (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: @@ -468,7 +468,7 @@ let tauto = let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g -and intros_with_rewrite_aux : Proof_type.tactic = +and intros_with_rewrite_aux : Tacmach.tactic = fun g -> let eq_ind = make_eq () in let sigma = project g in @@ -629,7 +629,7 @@ let rec reflexivity_with_destruct_cases g = *) -let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.tactic = +let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tactic = fun g -> (* We compute the types of the different mutually recursive lemmas in $\zeta$ normal form @@ -673,7 +673,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.ta using [f_equation] if it is recursive (that is the graph is infinite or unfold if the graph is finite *) - let rewrite_tac j ids : Proof_type.tactic = + let rewrite_tac j ids : Tacmach.tactic = let graph_def = graphs.(j) in let infos = try find_Function_infos (fst (destConst (project g) funcs.(j))) @@ -953,7 +953,7 @@ let revert_graph kn post_tac hid g = \end{enumerate} *) -let functional_inversion kn hid fconst f_correct : Proof_type.tactic = +let functional_inversion kn hid fconst f_correct : Tacmach.tactic = fun g -> let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in let sigma = project g in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index c75f7f868c..ba88563d3b 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -880,7 +880,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,pl,impls = Command.interp_mutual_inductive indl [] - false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in + false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 20abde82f2..8e12b239e8 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -30,7 +30,7 @@ open Nametab open Declare open Decl_kinds open Tacred -open Proof_type +open Goal open Pfedit open Glob_term open Pretyping @@ -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/funind/recdef.mli b/plugins/funind/recdef.mli index e1a072799e..f3d5e73320 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -2,10 +2,10 @@ open API (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : - Proof_type.tactic -> + Tacmach.tactic -> bool -> Names.Id.t list option -> - Proof_type.tactic + Tacmach.tactic val recursive_definition : bool -> Names.Id.t -> diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 07b8746fb2..50013f5583 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -17,7 +17,7 @@ open Stdarg open Extraargs open Names -DECLARE PLUGIN "coretactics" +DECLARE PLUGIN "ltac_plugin" (** Basic tactics *) @@ -324,11 +324,11 @@ let initial_atomic () = "fresh", TacArg(Loc.tag @@ TacFreshId []) ] -let () = Mltop.declare_cache_obj initial_atomic "coretactics" +let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin" (* First-class Ltac access to primitive blocks *) -let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; } +let initial_name s = { mltac_plugin = "ltac_plugin"; mltac_tactic = s; } let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; } let register_list_tactical name f = @@ -356,4 +356,4 @@ let initial_tacticals () = "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0]))); ] -let () = Mltop.declare_cache_obj initial_tacticals "coretactics" +let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin" 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..36df25cc77 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -28,7 +28,7 @@ open Equality open Misctypes open Proofview.Notations -DECLARE PLUGIN "extratactics" +DECLARE PLUGIN "ltac_plugin" (**********************************************************************) (* replace, discriminate, injection, simplify_eq *) @@ -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_auto.ml4 b/plugins/ltac/g_auto.ml4 index dfd8e88a91..6145e373b1 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -18,7 +18,7 @@ open Pcoq.Constr open Pltac open Hints -DECLARE PLUGIN "g_auto" +DECLARE PLUGIN "ltac_plugin" (* Hint bases *) diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 905cfd02a6..63451210ca 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -13,7 +13,7 @@ open Class_tactics open Stdarg open Tacarg -DECLARE PLUGIN "g_class" +DECLARE PLUGIN "ltac_plugin" (** Options: depth, debug and transparency settings. *) diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index 570cd4e694..dceefeaa13 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -17,7 +17,7 @@ open API open Eqdecide -DECLARE PLUGIN "g_eqdecide" +DECLARE PLUGIN "ltac_plugin" TACTIC EXTEND decide_equality | [ "decide" "equality" ] -> [ decideEqualityGoal ] diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index e6ddc5cc1b..3e6f420065 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -27,7 +27,7 @@ open Pcoq.Prim open Pcoq.Constr open Pltac -DECLARE PLUGIN "g_rewrite" +DECLARE PLUGIN "ltac_plugin" type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings 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/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack index af1c7149da..12b4c81fc4 100644 --- a/plugins/ltac/ltac_plugin.mlpack +++ b/plugins/ltac/ltac_plugin.mlpack @@ -21,7 +21,6 @@ G_auto G_class Rewrite G_rewrite -Tauto G_eqdecide G_tactic G_ltac 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..71f7082e70 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -13,13 +13,14 @@ open Hipattern open Names open Geninterp open Misctypes +open Ltac_plugin open Tacexpr open Tacinterp open Util open Tacticals.New open Proofview.Notations -let tauto_plugin = "tauto" +let tauto_plugin = "tauto_plugin" let () = Mltop.add_known_module tauto_plugin let assoc_var s ist = @@ -66,7 +67,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 +80,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/ltac/tauto_plugin.mlpack b/plugins/ltac/tauto_plugin.mlpack new file mode 100644 index 0000000000..b3618018ea --- /dev/null +++ b/plugins/ltac/tauto_plugin.mlpack @@ -0,0 +1 @@ +Tauto 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/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index d242264a91..51b99b9935 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -18,12 +18,12 @@ Module Type Int. Bind Scope Int_scope with t. - Parameter zero : t. - Parameter one : t. - Parameter plus : t -> t -> t. - Parameter opp : t -> t. - Parameter minus : t -> t -> t. - Parameter mult : t -> t -> t. + Parameter Inline zero : t. + Parameter Inline one : t. + Parameter Inline plus : t -> t -> t. + Parameter Inline opp : t -> t. + Parameter Inline minus : t -> t -> t. + Parameter Inline mult : t -> t -> t. Notation "0" := zero : Int_scope. Notation "1" := one : Int_scope. @@ -39,10 +39,10 @@ Module Type Int. (** Int should also be ordered: *) - Parameter le : t -> t -> Prop. - Parameter lt : t -> t -> Prop. - Parameter ge : t -> t -> Prop. - Parameter gt : t -> t -> Prop. + Parameter Inline le : t -> t -> Prop. + Parameter Inline lt : t -> t -> Prop. + Parameter Inline ge : t -> t -> Prop. + Parameter Inline gt : t -> t -> Prop. Notation "x <= y" := (le x y): Int_scope. Notation "x < y" := (lt x y) : Int_scope. Notation "x >= y" := (ge x y) : Int_scope. diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 1a53862ec4..60e6e7de79 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1016,7 +1016,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = Tactics.generalize (l_generalize_arg @ List.map EConstr.mkVar useful_hypnames) >> - Tactics.change_concl (EConstr.of_constr reified) >> + Tactics.convert_concl_no_check (EConstr.of_constr reified) Term.DEFAULTcast >> Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >> show_goal >> (if unsafe then diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index ac260e51ac..801fc46067 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -14,13 +14,13 @@ type atom_env= mutable env:(Term.constr*int) list} val make_form : atom_env -> - Proof_type.goal Evd.sigma -> EConstr.types -> Proof_search.form + Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form val make_hyps : atom_env -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> EConstr.types list -> EConstr.named_context -> (Names.Id.t * Proof_search.form) list -val rtauto_tac : Proof_type.tactic +val rtauto_tac : Tacmach.tactic diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index ee75d2908e..da21f64ab1 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,8 +153,8 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na ctx c = let open Term in - let vars = Universes.universes_of_constr c in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in + let vars = Univops.universes_of_constr c in + let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~univs:(Univ.ContextSet.to_context ctx) c), diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 0f4b86d10d..94eaa1d6aa 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -145,6 +145,6 @@ type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option) (* OOP : these are general shortcuts *) type gist = Tacintern.glob_sign type ist = Tacinterp.interp_sign -type goal = Proof_type.goal +type goal = Goal.goal type 'a sigma = 'a Evd.sigma -type v82tac = Proof_type.tactic +type v82tac = Tacmach.tactic diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index b0e98bdb47..20a1263d24 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -10,7 +10,7 @@ open API -val apply_top_tac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma +val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val inner_ssrapplytac : Ssrast.ssrterm list -> @@ -19,4 +19,4 @@ val inner_ssrapplytac : list list -> Ssrast.ssrhyps -> Ssrast.ist -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d389f70859..411ce6853c 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 = { @@ -960,7 +960,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t)); - Refiner.refiner (Proof_type.Refine (EConstr.Unsafe.to_constr t)) gl + Tacmach.refine_no_check t gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 7a4b47a462..f611685769 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -9,9 +9,9 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) open API +open Tacmach open Names open Environ -open Proof_type open Evd open Constrexpr open Ssrast @@ -122,11 +122,11 @@ val intern_term : ssrterm -> Glob_term.glob_constr val pf_intern_term : - Tacinterp.interp_sign -> Proof_type.goal Evd.sigma -> + Tacinterp.interp_sign -> Goal.goal Evd.sigma -> ssrterm -> Glob_term.glob_constr val interp_term : - Tacinterp.interp_sign -> Proof_type.goal Evd.sigma -> + Tacinterp.interp_sign -> Goal.goal Evd.sigma -> ssrterm -> evar_map * EConstr.t val interp_wit : @@ -136,28 +136,28 @@ val interp_hyp : ist -> goal sigma -> ssrhyp -> evar_map * ssrhyp val interp_hyps : ist -> goal sigma -> ssrhyps -> evar_map * ssrhyps val interp_refine : - Tacinterp.interp_sign -> Proof_type.goal Evd.sigma -> + Tacinterp.interp_sign -> Goal.goal Evd.sigma -> Glob_term.glob_constr -> evar_map * (evar_map * EConstr.constr) val interp_open_constr : - Tacinterp.interp_sign -> Proof_type.goal Evd.sigma -> + Tacinterp.interp_sign -> Goal.goal Evd.sigma -> Tacexpr.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) val pf_e_type_of : - Proof_type.goal Evd.sigma -> - EConstr.constr -> Proof_type.goal Evd.sigma * EConstr.types + Goal.goal Evd.sigma -> + EConstr.constr -> Goal.goal Evd.sigma * EConstr.types val splay_open_constr : - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> evar_map * EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t -val isAppInd : Proof_type.goal Evd.sigma -> EConstr.types -> bool +val isAppInd : Goal.goal Evd.sigma -> EConstr.types -> bool val interp_view_nbimps : Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> Glob_term.glob_constr -> int + Goal.goal Evd.sigma -> Glob_term.glob_constr -> int val interp_nbargs : Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> Glob_term.glob_constr -> int + Goal.goal Evd.sigma -> Glob_term.glob_constr -> int val mk_term : ssrtermkind -> 'b -> ssrtermkind * (Glob_term.glob_constr * 'b option) @@ -169,20 +169,20 @@ val mk_internal_id : string -> Id.t val mk_tagged_id : string -> int -> Id.t val mk_evar_name : int -> Name.t val ssr_anon_hyp : string -val pf_type_id : Proof_type.goal Evd.sigma -> EConstr.types -> Id.t +val pf_type_id : Goal.goal Evd.sigma -> EConstr.types -> Id.t val pf_abs_evars : - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> evar_map * EConstr.t -> int * EConstr.t * Evar.t list * UState.t val pf_abs_evars2 : (* ssr2 *) - Proof_type.goal Evd.sigma -> Evar.t list -> + Goal.goal Evd.sigma -> Evar.t list -> evar_map * EConstr.t -> int * EConstr.t * Evar.t list * UState.t val pf_abs_cterm : - Proof_type.goal Evd.sigma -> int -> EConstr.t -> EConstr.t + Goal.goal Evd.sigma -> int -> EConstr.t -> EConstr.t val pf_merge_uc : UState.t -> 'a Evd.sigma -> 'a Evd.sigma @@ -190,21 +190,21 @@ val pf_merge_uc_of : evar_map -> 'a Evd.sigma -> 'a Evd.sigma val constr_name : evar_map -> EConstr.t -> Name.t val pf_type_of : - Proof_type.goal Evd.sigma -> - Term.constr -> Proof_type.goal Evd.sigma * Term.types + Goal.goal Evd.sigma -> + Term.constr -> Goal.goal Evd.sigma * Term.types val pfe_type_of : - Proof_type.goal Evd.sigma -> - EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types + Goal.goal Evd.sigma -> + EConstr.t -> Goal.goal Evd.sigma * EConstr.types val pf_abs_prod : Name.t -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> EConstr.t -> - EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types + EConstr.t -> Goal.goal Evd.sigma * EConstr.types val pf_mkprod : - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> EConstr.t -> ?name:Name.t -> - EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types + EConstr.t -> Goal.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option val mkSsrRef : string -> Globnames.global_reference @@ -213,15 +213,15 @@ val mkSsrConst : env -> evar_map -> evar_map * EConstr.t val pf_mkSsrConst : string -> - Proof_type.goal Evd.sigma -> - EConstr.t * Proof_type.goal Evd.sigma + Goal.goal Evd.sigma -> + EConstr.t * Goal.goal Evd.sigma val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : Globnames.global_reference -> - Proof_type.goal Evd.sigma -> - Term.constr * Proof_type.goal Evd.sigma + Goal.goal Evd.sigma -> + Term.constr * Goal.goal Evd.sigma val is_discharged_id : Id.t -> bool val mk_discharged_id : Id.t -> Id.t @@ -230,15 +230,15 @@ val has_discharged_tag : string -> bool val ssrqid : string -> Libnames.qualid val new_tmp_id : tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx -val mk_anon_id : string -> Proof_type.goal Evd.sigma -> Id.t +val mk_anon_id : string -> Goal.goal Evd.sigma -> Id.t val pf_abs_evars_pirrel : - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> evar_map * Term.constr -> int * Term.constr -val pf_nbargs : Proof_type.goal Evd.sigma -> EConstr.t -> int +val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int val gen_tmp_ids : ?ist:Geninterp.interp_sign -> - (Proof_type.goal * tac_ctx) Evd.sigma -> - (Proof_type.goal * tac_ctx) list Evd.sigma + (Goal.goal * tac_ctx) Evd.sigma -> + (Goal.goal * tac_ctx) list Evd.sigma val ssrevaltac : Tacinterp.interp_sign -> Tacinterp.Value.t -> Proofview.V82.tac @@ -258,23 +258,23 @@ val ssrautoprop_tac : val mkProt : EConstr.t -> EConstr.t -> - Proof_type.goal Evd.sigma -> - EConstr.t * Proof_type.goal Evd.sigma + Goal.goal Evd.sigma -> + EConstr.t * Goal.goal Evd.sigma val mkEtaApp : EConstr.t -> int -> int -> EConstr.t val mkRefl : EConstr.t -> EConstr.t -> - Proof_type.goal Evd.sigma -> EConstr.t * Proof_type.goal Evd.sigma + Goal.goal Evd.sigma -> EConstr.t * Goal.goal Evd.sigma val discharge_hyp : Id.t * (Id.t * string) -> - Proof_type.goal Evd.sigma -> Evar.t list Evd.sigma + Goal.goal Evd.sigma -> Evar.t list Evd.sigma val clear_wilds_and_tmp_and_delayed_ids : - (Proof_type.goal * tac_ctx) Evd.sigma -> - (Proof_type.goal * tac_ctx) list Evd.sigma + (Goal.goal * tac_ctx) Evd.sigma -> + (Goal.goal * tac_ctx) list Evd.sigma val view_error : string -> ssrterm -> 'a @@ -284,14 +284,14 @@ val top_id : Id.t val pf_abs_ssrterm : ?resolve_typeclasses:bool -> ist -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> ssrterm -> evar_map * EConstr.t * UState.t * int val pf_interp_ty : ?resolve_typeclasses:bool -> Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> Ssrast.ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) -> int * EConstr.t * EConstr.t * UState.t @@ -309,12 +309,12 @@ exception NotEnoughProducts val pf_saturate : ?beta:bool -> ?bi_types:bool -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> EConstr.constr -> ?ty:EConstr.types -> int -> EConstr.constr * EConstr.types * (int * EConstr.constr) list * - Proof_type.goal Evd.sigma + Goal.goal Evd.sigma val saturate : ?beta:bool -> ?bi_types:bool -> @@ -338,32 +338,32 @@ type name_hint = (int * EConstr.types array) option ref val gentac : (Geninterp.interp_sign -> (Ssrast.ssrdocc) * - Ssrmatching_plugin.Ssrmatching.cpattern -> Proof_type.tactic) + Ssrmatching_plugin.Ssrmatching.cpattern -> Tacmach.tactic) val genstac : ((Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern) list * Ssrast.ssrhyp list -> - Tacinterp.interp_sign -> Proof_type.tactic + Tacinterp.interp_sign -> Tacmach.tactic val pf_interp_gen : Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> bool -> (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern -> EConstr.t * EConstr.t * Ssrast.ssrhyp list * - Proof_type.goal Evd.sigma + Goal.goal Evd.sigma val pf_interp_gen_aux : Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> bool -> (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern -> bool * Ssrmatching_plugin.Ssrmatching.pattern * EConstr.t * EConstr.t * Ssrast.ssrhyp list * UState.t * - Proof_type.goal Evd.sigma + Goal.goal Evd.sigma val is_name_in_ipats : Id.t -> ssripats -> bool @@ -386,12 +386,12 @@ val interp_clr : val genclrtac : EConstr.constr -> - EConstr.constr list -> Ssrast.ssrhyp list -> Proof_type.tactic + EConstr.constr list -> Ssrast.ssrhyp list -> Tacmach.tactic val cleartac : ssrhyps -> v82tac -val tclMULT : int * ssrmmod -> Proof_type.tactic -> Proof_type.tactic +val tclMULT : int * ssrmmod -> Tacmach.tactic -> Tacmach.tactic -val unprotecttac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma +val unprotecttac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val abs_wgen : bool -> @@ -401,8 +401,8 @@ val abs_wgen : ((Ssrast.ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option -> - Proof_type.goal Evd.sigma * EConstr.t list * EConstr.t -> - Proof_type.goal Evd.sigma * EConstr.t list * EConstr.t + Goal.goal Evd.sigma * EConstr.t list * EConstr.t -> + Goal.goal Evd.sigma * EConstr.t list * EConstr.t val clr_of_wgen : ssrhyps * ((ssrhyp_or_id * 'a) * 'b option) option -> diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index 8dc28d8b75..825b4758e3 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -32,23 +32,23 @@ val ssrelim : (?ist:Ltac_plugin.Tacinterp.interp_sign -> 'a -> Ssrast.ssripat option -> - (Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma) -> - bool -> Ssrast.ssrhyp list -> Proof_type.tactic) -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + (Goal.goal Evd.sigma -> Goal.goal list Evd.sigma) -> + bool -> Ssrast.ssrhyp list -> Tacmach.tactic) -> + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val elimtac : EConstr.constr -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val casetac : EConstr.constr -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val is_injection_case : EConstr.t -> Proof_type.goal Evd.sigma -> bool +val is_injection_case : EConstr.t -> Goal.goal Evd.sigma -> bool val perform_injection : EConstr.constr -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val ssrscasetac : bool -> EConstr.constr -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index f712002c1f..f9ab5d74fe 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -25,12 +25,12 @@ val mkclr : ssrclear -> ssrdocc val nodocc : ssrdocc val noclr : ssrdocc -val simpltac : Ssrast.ssrsimpl -> Proof_type.tactic +val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic val newssrcongrtac : int * Ssrast.ssrterm -> Ltac_plugin.Tacinterp.interp_sign -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val mk_rwarg : @@ -45,7 +45,7 @@ val ssrinstancesofrule : Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssrdir -> Ssrast.ssrterm -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val ssrrewritetac : Ltac_plugin.Tacinterp.interp_sign -> @@ -53,11 +53,11 @@ val ssrrewritetac : (((Ssrast.ssrhyps option * Ssrmatching.occ) * Ssrmatching.rpattern option) * (ssrwkind * Ssrast.ssrterm))) - list -> Proof_type.tactic + list -> Tacmach.tactic -val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Proof_type.tactic +val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic val unlocktac : Ltac_plugin.Tacinterp.interp_sign -> (Ssrmatching.occ * Ssrast.ssrterm) list -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index ead361745d..7f254074c7 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -36,7 +36,7 @@ val ssrabstract : val basecuttac : string -> - EConstr.t -> Proof_type.goal Evd.sigma -> Evar.t list Evd.sigma + EConstr.t -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma val wlogtac : Ltac_plugin.Tacinterp.interp_sign -> @@ -52,7 +52,7 @@ val wlogtac : Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> bool -> [< `Gen of Names.Id.t option option | `NoGen > `NoGen ] -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val sufftac : Ssrast.ist -> @@ -62,5 +62,5 @@ val sufftac : (Ssrast.ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option))) * (bool * Tacinterp.Value.t option list)) -> - Proof_type.tactic + Tacmach.tactic diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 4a9dddd2ba..06bbd749e6 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 = @@ -175,10 +175,10 @@ let move_top_with_view ~next c r v = type block_names = (int * EConstr.types array) option -let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Proof_type.tactic), +let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic), (tclEQINTROS : ?ind:block_names ref -> ?ist:Tacinterp.interp_sign -> - Proof_type.tactic -> Proof_type.tactic -> ssripats -> - Proof_type.tactic) + Tacmach.tactic -> Tacmach.tactic -> ssripats -> + Tacmach.tactic) = let rec ipattac ?ist ~next p : tac_ctx tac_a = fun gl -> diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index 5f5c7f34a4..aefdc8e111 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -36,10 +36,10 @@ val elim_intro_tac : ?ist:Tacinterp.interp_sign -> [> `EConstr of 'a * 'b * EConstr.t ] -> Ssrast.ssripat option -> - Proof_type.tactic -> + Tacmach.tactic -> bool -> Ssrast.ssrhyp list -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma (* "move=> top; tac top; clear top" respecting the speed *) val with_top : (EConstr.t -> v82tac) -> tac_ctx tac_a @@ -51,17 +51,17 @@ val ssrmovetac : (((Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear) * Ssrast.ssripats)) -> - Proof_type.tactic + Tacmach.tactic -val movehnftac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma +val movehnftac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val with_dgens : (Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear -> ((Ssrast.ssrdocc * Ssrmatching.cpattern) list -> Ssrast.ssrdocc * Ssrmatching.cpattern -> - Ltac_plugin.Tacinterp.interp_sign -> Proof_type.tactic) -> - Ltac_plugin.Tacinterp.interp_sign -> Proof_type.tactic + Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic) -> + Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic val ssrcasetac : Ltac_plugin.Tacinterp.interp_sign -> @@ -69,7 +69,7 @@ val ssrcasetac : (Ssrast.ssripat option * (((Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear) * Ssrast.ssripats)) -> - Proof_type.tactic + Tacmach.tactic val ssrapplytac : Tacinterp.interp_sign -> @@ -79,5 +79,5 @@ val ssrapplytac : (Ssrast.ssrtermkind * Tacexpr.glob_constr_and_expr)) list list * Ssrast.ssrhyps) * Ssrast.ssripats)) -> - Proof_type.tactic + Tacmach.tactic 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 diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 9207b9e437..8da9bc72bc 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -12,7 +12,7 @@ open API open Ssrast val pp_term : - Proof_type.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds + Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds val pr_spc : unit -> Pp.std_ppcmds val pr_bar : unit -> Pp.std_ppcmds diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index 1d18871387..297cfdfdc0 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -17,7 +17,7 @@ val tclSEQAT : int Misctypes.or_var * (('a * Ltac_plugin.Tacinterp.Value.t option list) * Ltac_plugin.Tacinterp.Value.t option) -> - Proof_type.tactic + Tacmach.tactic val tclCLAUSES : Ltac_plugin.Tacinterp.interp_sign -> @@ -27,7 +27,7 @@ val tclCLAUSES : Ssrmatching_plugin.Ssrmatching.cpattern option) option) list * Ssrast.ssrclseq -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val hinttac : Tacinterp.interp_sign -> @@ -42,5 +42,5 @@ val ssrdotac : Ssrmatching_plugin.Ssrmatching.cpattern option) option) list * Ssrast.ssrclseq) -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 91e40f3684..cc142e091c 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -80,7 +80,7 @@ let interp_view ist si env sigma gv v rid = snd (view_with (if view_nbimps < 0 then [] else viewtab.(0))) -let with_view ist ~next si env (gl0 : (Proof_type.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr = +let with_view ist ~next si env (gl0 : (Goal.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr = let c2r ist x = { ist with lfun = Id.Map.add top_id (Value.of_constr x) ist.lfun } in let terminate (sigma, c') = diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index c2bf12cb63..1853bc35dc 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -3,11 +3,11 @@ open API open Grammar_API +open Goal open Genarg open Tacexpr open Environ open Evd -open Proof_type open Term (** ******** Small Scale Reflection pattern matching facilities ************* *) |