diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/cc/ccalgo.ml | 16 | ||||
-rw-r--r-- | plugins/cc/cctac.ml | 1 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 2 | ||||
-rw-r--r-- | plugins/firstorder/g_ground.ml4 | 11 | ||||
-rw-r--r-- | plugins/firstorder/ground.ml | 2 | ||||
-rw-r--r-- | plugins/firstorder/rules.ml | 4 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 3 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 1 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 3 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 1 | ||||
-rw-r--r-- | plugins/ltac/extratactics.ml4 | 38 | ||||
-rw-r--r-- | plugins/ltac/g_auto.ml4 | 15 | ||||
-rw-r--r-- | plugins/ltac/g_ltac.ml4 | 18 | ||||
-rw-r--r-- | plugins/ltac/g_obligations.ml4 | 12 | ||||
-rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 27 | ||||
-rw-r--r-- | plugins/ltac/rewrite.ml | 4 | ||||
-rw-r--r-- | plugins/ltac/rewrite.mli | 2 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 54 | ||||
-rw-r--r-- | plugins/quote/quote.ml | 2 | ||||
-rw-r--r-- | plugins/romega/const_omega.ml | 13 | ||||
-rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
-rw-r--r-- | plugins/ssr/ssrfwd.ml | 7 | ||||
-rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 11 |
24 files changed, 146 insertions, 105 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index faabd7c14..ccef9ab96 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -12,13 +12,13 @@ open CErrors open Pp -open Goptions open Names -open Term +open Sorts open Constr open Vars -open Tacmach open Evd +open Goptions +open Tacmach open Util let init_size=5 @@ -437,7 +437,7 @@ and make_app l=function and applist_proj c l = match c with | Symb s -> applist_projection s l - | _ -> applistc (constr_of_term c) l + | _ -> Term.applistc (constr_of_term c) l and applist_projection c l = match Constr.kind c with | Const c when Environ.is_projection (fst c) (Global.env()) -> @@ -447,10 +447,10 @@ and applist_projection c l = let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *) let pb = Environ.lookup_projection p (Global.env()) in let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in - it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx + Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx | hd :: tl -> - applistc (mkProj (p, hd)) tl) - | _ -> applistc c l + Term.applistc (mkProj (p, hd)) tl) + | _ -> Term.applistc c l let rec canonize_name sigma c = let c = EConstr.Unsafe.to_constr c in @@ -838,7 +838,7 @@ let complete_one_class state i= let _args = List.map (fun i -> constr_of_term (term state.uf i)) pac.args in - let typ = prod_applist _c (List.rev _args) in + let typ = Term.prod_applist _c (List.rev _args) in let ct = app (term state.uf i) typ pac.arity in state.uf.epsilons <- pac :: state.uf.epsilons; ignore (add_term state ct) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 7dec34d4d..8642df684 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -12,7 +12,6 @@ open Evd open Names open Inductiveops open Declarations -open Term open Constr open EConstr open Vars diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 995d5fd19..5903733a6 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -486,7 +486,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str "Please load library " ++ pr_dirpath dp ++ str " first.") + err (str "Please load library " ++ DirPath.print dp ++ str " first.") | _ -> () end | _ -> () diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 1e7da3250..938bec25b 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -65,11 +65,14 @@ let default_intuition_tac = let (set_default_solver, default_solver, print_default_solver) = Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" -VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ - set_default_solver - (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (Tacintern.glob_tactic t) ] + fun ~atts ~st -> let open Vernacinterp in + set_default_solver + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t); + st + ] END VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index f660ba734..d46201335 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -11,7 +11,7 @@ open Formula open Sequent open Rules open Instances -open Term +open Constr open Tacmach.New open Tacticals.New diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index d6309b057..1a6eba8c6 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -235,8 +235,8 @@ let constant str = Universes.constr_of_global @@ Coqlib.coq_reference "User" ["Init";"Logic"] str let defined_connectives=lazy - [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not"))); - AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))] + [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not"))); + AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 29e824f44..62ca70626 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,7 +1,7 @@ open Printer open CErrors open Util -open Term +open Constr open EConstr open Vars open Namegen diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 3899bc709..996e2b6af 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,7 +1,8 @@ open Printer open CErrors -open Util open Term +open Sorts +open Util open Constr open Vars open Namegen diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index d04b7a33d..fa4353630 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1,7 +1,6 @@ open Printer open Pp open Names -open Term open Constr open Vars open Glob_term diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f01b6669d..9e22ad306 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,7 +1,8 @@ open CErrors +open Sorts open Util open Names -open Term +open Constr open EConstr open Pp open Indfun_common diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 04d729b10..3089ec470 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -9,7 +9,6 @@ module CVars = Vars -open Term open Constr open EConstr open Vars diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 71db919ef..d6cfa3cf9 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -320,24 +320,44 @@ let project_hint pri l2r r = let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) -let add_hints_iff l2r lc n bl = - let l = Locality.LocalityFixme.consume () in - Hints.add_hints (Locality.make_module_locality l) bl +let add_hints_iff ?locality l2r lc n bl = + Hints.add_hints (Locality.make_module_locality locality) bl (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc)) -VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> - [ add_hints_iff true lc n bl ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality true lc n bl; + st + end + ] | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> - [ add_hints_iff true lc n ["core"] ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality true lc n ["core"]; + st + end + ] END -VERNAC COMMAND EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF + +VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> - [ add_hints_iff false lc n bl ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality false lc n bl; + st + end + ] | [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> - [ add_hints_iff false lc n ["core"] ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality false lc n ["core"]; + st + end + ] END (**********************************************************************) diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 84e79d8ab..90a44708f 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -190,7 +190,7 @@ END let pr_hints_path prc prx pry c = Hints.pp_hints_path c let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c let glob_hints_path ist = Hints.glob_hints_path - + ARGUMENT EXTEND hints_path PRINTED BY pr_hints_path @@ -214,10 +214,15 @@ ARGUMENT EXTEND opthints | [ ] -> [ None ] END -VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (match dbnames with None -> ["core"] | Some l -> l) entry ] + fun ~atts ~st -> begin + let open Vernacinterp in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + Hints.add_hints (Locality.make_section_locality atts.locality) + (match dbnames with None -> ["core"] | Some l -> l) entry; + st + end + ] END diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 116152568..34fea6175 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -469,13 +469,13 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ] END -VERNAC COMMAND EXTEND VernacTacticNotation +VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => [ VtUnknown, VtNow ] -> - [ - let l = Locality.LocalityFixme.consume () in - let n = Option.default 0 n in - Tacentries.add_tactic_notation (Locality.make_module_locality l) n r e + [ fun ~atts ~st -> let open Vernacinterp in + let n = Option.default 0 n in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; + st ] END @@ -512,15 +512,15 @@ PRINTED BY pr_tacdef_body | [ tacdef_body(t) ] -> [ t ] END -VERNAC COMMAND EXTEND VernacDeclareTacticDefinition +VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ((_,r),_) -> r | TacticRedefinition (Ident (_,r),_) -> r | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater - ] -> [ - let lc = Locality.LocalityFixme.consume () in - Tacentries.register_ltac (Locality.make_module_locality lc) l + ] -> [ fun ~atts ~st -> let open Vernacinterp in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; + st ] END diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index fea9e837b..f6cc3833a 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -123,11 +123,15 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF | [ "Admit" "Obligations" ] -> [ admit_obligations None ] END -VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - set_default_tactic - (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (Tacintern.glob_tactic t) ] + fun ~atts ~st -> begin + let open Vernacinterp in + set_default_tactic + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t); + st + end] END open Pp diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 91abe1019..ea1808a25 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -243,22 +243,37 @@ VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] END -VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ] + [ fun ~atts ~st -> let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; + st + ] | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ] + [ fun ~atts ~st -> let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; + st + ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] - -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; + st + ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; + st + ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; + st + ] END TACTIC EXTEND setoid_symmetry diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c63492d1b..14b0742a7 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1800,9 +1800,9 @@ let declare_instance_trans global binders a aeq n lemma = in anew_instance global binders instance [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)] -let declare_relation ?(binders=[]) a aeq n refl symm trans = +let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) in + let global = not (Locality.make_section_locality locality) in let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in ignore(anew_instance global binders instance []); match (refl,symm,trans) with diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 1306c590b..17e7244b3 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -75,7 +75,7 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : +val declare_relation : ?locality:bool -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ff69ddefb..869284246 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/quote/quote.ml b/plugins/quote/quote.ml index 96bf31b11..0ea8904f2 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -104,7 +104,7 @@ open CErrors open Util open Names -open Term +open Constr open EConstr open Pattern open Patternops diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 5397b0065..337510ef1 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -7,7 +7,6 @@ *************************************************************************) open Names -open Term open Constr let module_refl_name = "ReflOmegaCore" @@ -198,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") @@ -238,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") @@ -286,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/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 274c7110c..bd9633afb 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -342,7 +342,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let sort = elimination_sort_of_goal gl in let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) - let elim, _ = Term.destConst elim in + let elim, _ = destConst elim in let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index a707226cd..5c1b399a8 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -8,11 +8,12 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open Pp open Names +open Constr open Tacmach open Ssrmatching_plugin.Ssrmatching - open Ssrprinters open Ssrcommon open Ssrtacticals @@ -30,10 +31,6 @@ let ssrposetac ist (id, (_, t)) gl = let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in posetac id t (pf_merge_uc ucst gl) -open Pp -open Term -open Constr - let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl = let pat = interp_cpattern ist gl pat (Option.map snd pty) in let cl, sigma, env = pf_concl gl, project gl, pf_env gl in diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index cd614fee9..7385ed84c 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -158,11 +158,14 @@ let declare_one_prenex_implicit locality f = | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] -VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF | [ "Prenex" "Implicits" ne_global_list(fl) ] - -> [ let locality = - Locality.make_section_locality (Locality.LocalityFixme.consume ()) in - List.iter (declare_one_prenex_implicit locality) fl ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + let locality = Locality.make_section_locality atts.locality in + List.iter (declare_one_prenex_implicit locality) fl; + st + ] END (* Vernac grammar visibility patch *) |