diff options
34 files changed, 425 insertions, 326 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 65a8a0cb88..b1a805b59e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -225,6 +225,13 @@ build:egde:dune:dev: OPAM_SWITCH: edge DUNE_TARGET: world +build:base+async: + <<: *build-template + stage: test + variables: + COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" + COQUSERFLAGS: "-async-proofs on" + windows64: <<: *windows-template variables: diff --git a/Makefile.build b/Makefile.build index ec9b81dba4..0a73562467 100644 --- a/Makefile.build +++ b/Makefile.build @@ -44,6 +44,9 @@ NO_RECALC_DEPS ?= # Non-empty runs the checker on all produced .vo files: VALIDATE ?= +# When non-empty, passed as extra arguments to coqtop/coqc: +COQUSERFLAGS ?= + # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -191,7 +194,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # the output format of the unix command time. For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) +COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index cda369fb1b..470d07b27d 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -13,4 +13,4 @@ eval "$(opam env)" opam install -y num ocamlfind ounit # Full regular Coq Build -cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte # && make -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/doc/changes.md b/dev/doc/changes.md index c0f15f02a5..e7d4b605c7 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -52,6 +52,26 @@ Macros: where `atts : Vernacexpr.vernac_flags` was bound in the expression and had to be manually parsed. +Libobject + +- A Higher-level API for objects with fixed scope was introduced. It supports the following kinds of objects: + + * Local objects, meaning that objects cannot be imported from outside. + * Global objects, meaning that they can be imported (by importing the module that contains the object). + * Superglobal objects, meaning that objects survive to closing a module, and + are imported when the file which contains them is Required (even without + Import). + * Objects that survive section closing or don't (see `nodischarge` variants, + however we discourage defining such objects) + + This API is made of the following functions: + * `Libobject.local_object` + * `Libobject.local_object_nodischarge` + * `Libobject.global_object` + * `Libobject.global_object_nodischarge` + * `Libobject.superglobal_object` + * `Libobject.superglobal_object_nodischarge` + ## Changes between Coq 8.8 and Coq 8.9 ### ML API diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index ad80cb62e1..59602581c7 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3425,7 +3425,9 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. cmdv:: Hint @hint_definition - No database name is given: the hint is registered in the core database. + No database name is given: the hint is registered in the ``core`` database. + + .. deprecated:: 8.10 .. cmdv:: Local Hint @hint_definition : {+ @ident} diff --git a/ide/idetop.ml b/ide/idetop.ml index 8b3b566f9c..6a4c7603ee 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -219,7 +219,7 @@ let goals () = | Some oldp -> let (_,_,_,_,osigma) = Proof.proof oldp in (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma } - with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (6)")) + with Not_found -> None) (* will appear as a new goal *) | None -> None in let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 40922b5c35..7aa85a0810 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1527,8 +1527,8 @@ let drop_notations_pattern looked_for genv = try match Nametab.locate_extended qid with | SynDef sp -> - let (vars,a) = Syntax_def.search_syntactic_definition sp in - (match a with + let filter (vars,a) = + try match a with | NRef g -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; @@ -1549,7 +1549,9 @@ let drop_notations_pattern looked_for genv = let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in let (_,argscs) = find_remaining_scopes pats1 pats2 g in Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2) - | _ -> raise Not_found) + | _ -> raise Not_found + with Not_found -> None in + Syntax_def.search_filtered_syntactic_definition filter sp | TrueGlobal g -> test_kind top g; Dumpglob.add_glob ?loc:qid.loc g; diff --git a/interp/declare.ml b/interp/declare.ml index a0ebc3775e..6778fa1e7a 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -445,11 +445,9 @@ let assumption_message id = (** Monomorphic universes need to survive sections. *) let input_universe_context : Univ.ContextSet.t -> Libobject.obj = - declare_object - { (default_object "Monomorphic section universes") with - cache_function = (fun (na, uctx) -> Global.push_context_set false uctx); - discharge_function = (fun (_, x) -> Some x); - classify_function = (fun a -> Dispose) } + declare_object @@ local_object "Monomorphic section universes" + ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) + ~discharge:(fun (_, x) -> Some x) let declare_universe_context poly ctx = if poly then diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index b73d238c22..49273c4146 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -105,3 +105,10 @@ let search_syntactic_definition ?loc kn = let def = out_pat pat in verbose_compat ?loc kn def v; def + +let search_filtered_syntactic_definition ?loc filter kn = + let pat,v = KNmap.find kn !syntax_table in + let def = out_pat pat in + let res = filter def in + (match res with Some _ -> verbose_compat ?loc kn def v | None -> ()); + res diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index c5b6655ff8..77873f8f67 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -19,3 +19,6 @@ val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation + +val search_filtered_syntactic_definition : ?loc:Loc.t -> + (syndef_interpretation -> 'a option) -> KerName.t -> 'a option diff --git a/library/keys.ml b/library/keys.ml index 53447a679a..58883ccc88 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -100,18 +100,13 @@ let discharge_keys (_,(k,k')) = | Some x, Some y -> Some (x, y) | _ -> None -let rebuild_keys (ref,ref') = (ref, ref') - type key_obj = key * key let inKeys : key_obj -> obj = - declare_object {(default_object "KEYS") with - cache_function = cache_keys; - load_function = load_keys; - subst_function = subst_keys; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_keys; - rebuild_function = rebuild_keys } + declare_object @@ superglobal_object "KEYS" + ~cache:cache_keys + ~subst:(Some subst_keys) + ~discharge:discharge_keys let declare_equiv_keys ref ref' = Lib.add_anonymous_leaf (inKeys (ref,ref')) diff --git a/library/libobject.ml b/library/libobject.ml index c153e9a09a..3d17b4a605 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -129,3 +129,46 @@ let rebuild_object lobj = apply_dyn_fun (fun d -> d.dyn_rebuild_function lobj) lobj let dump = Dyn.dump + +let local_object_nodischarge s ~cache = + { (default_object s) with + cache_function = cache; + classify_function = (fun _ -> Dispose); + } + +let local_object s ~cache ~discharge = + { (local_object_nodischarge s ~cache) with + discharge_function = discharge } + +let global_object_nodischarge s ~cache ~subst = + let import i o = if Int.equal i 1 then cache o in + { (default_object s) with + cache_function = cache; + open_function = import; + subst_function = (match subst with + | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!") + | Some subst -> subst; + ); + classify_function = + if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o); + } + +let global_object s ~cache ~subst ~discharge = + { (global_object_nodischarge s ~cache ~subst) with + discharge_function = discharge } + +let superglobal_object_nodischarge s ~cache ~subst = + { (default_object s) with + load_function = (fun _ x -> cache x); + cache_function = cache; + subst_function = (match subst with + | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!") + | Some subst -> subst; + ); + classify_function = + if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o); + } + +let superglobal_object s ~cache ~subst ~discharge = + { (superglobal_object_nodischarge s ~cache ~subst) with + discharge_function = discharge } diff --git a/library/libobject.mli b/library/libobject.mli index 32ffc5b79e..00515bd273 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -119,6 +119,51 @@ val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj +(** Higher-level API for objects with fixed scope. + +- Local means that the object cannot be imported from outside. +- Global means that it can be imported (by importing the module that contains the +object). +- Superglobal means that the object survives to closing a module, and is imported +when the file which contains it is Required (even without Import). +- With the nodischarge variants, the object does not survive section closing. + With the normal variants, it does. + +We recommend to avoid declaring superglobal objects and using the nodischarge +variants. +*) + +val local_object : string -> + cache:(object_name * 'a -> unit) -> + discharge:(object_name * 'a -> 'a option) -> + 'a object_declaration + +val local_object_nodischarge : string -> + cache:(object_name * 'a -> unit) -> + 'a object_declaration + +val global_object : string -> + cache:(object_name * 'a -> unit) -> + subst:(Mod_subst.substitution * 'a -> 'a) option -> + discharge:(object_name * 'a -> 'a option) -> + 'a object_declaration + +val global_object_nodischarge : string -> + cache:(object_name * 'a -> unit) -> + subst:(Mod_subst.substitution * 'a -> 'a) option -> + 'a object_declaration + +val superglobal_object : string -> + cache:(object_name * 'a -> unit) -> + subst:(Mod_subst.substitution * 'a -> 'a) option -> + discharge:(object_name * 'a -> 'a option) -> + 'a object_declaration + +val superglobal_object_nodischarge : string -> + cache:(object_name * 'a -> unit) -> + subst:(Mod_subst.substitution * 'a -> 'a) option -> + 'a object_declaration + (** {6 Debug} *) val dump : unit -> (int * string) list diff --git a/parsing/tok.ml b/parsing/tok.ml index 91b4f25ba3..c0d5b6742d 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -36,12 +36,24 @@ let equal t1 t2 = match t1, t2 with | EOI, EOI -> true | _ -> false -let extract_string = function +let extract_string diff_mode = function | KEYWORD s -> s | IDENT s -> s - | STRING s -> s + | STRING s -> + if diff_mode then + let escape_quotes s = + let len = String.length s in + let buf = Buffer.create len in + for i = 0 to len-1 do + let ch = String.get s i in + Buffer.add_char buf ch; + if ch = '"' then Buffer.add_char buf '"' else () + done; + Buffer.contents buf + in + "\"" ^ (escape_quotes s) ^ "\"" else s | PATTERNIDENT s -> s - | FIELD s -> s + | FIELD s -> if diff_mode then "." ^ s else s | INT s -> s | LEFTQMARK -> "?" | BULLET s -> s diff --git a/parsing/tok.mli b/parsing/tok.mli index 55fcd33272..5750096a28 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -22,7 +22,8 @@ type t = | EOI val equal : t -> t -> bool -val extract_string : t -> string +(* pass true for diff_mode *) +val extract_string : bool -> t -> string val to_string : t -> string (* Needed to fit Camlp5 signature *) val print : Format.formatter -> t -> unit diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 16890ea260..2058837b8e 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -621,10 +621,9 @@ let lang_ref = Summary.ref Ocaml ~name:"ExtrLang" let lang () = !lang_ref let extr_lang : lang -> obj = - declare_object - {(default_object "Extraction Lang") with - cache_function = (fun (_,l) -> lang_ref := l); - load_function = (fun _ (_,l) -> lang_ref := l)} + declare_object @@ superglobal_object_nodischarge "Extraction Lang" + ~cache:(fun (_,l) -> lang_ref := l) + ~subst:None let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) @@ -648,15 +647,10 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) let inline_extraction : bool * GlobRef.t list -> obj = - declare_object - {(default_object "Extraction Inline") with - cache_function = (fun (_,(b,l)) -> add_inline_entries b l); - load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); - classify_function = (fun o -> Substitute o); - discharge_function = (fun (_,x) -> Some x); - subst_function = - (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) - } + declare_object @@ superglobal_object "Extraction Inline" + ~cache:(fun (_,(b,l)) -> add_inline_entries b l) + ~subst:(Some (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))) + ~discharge:(fun (_,x) -> Some x) (* Grammar entries. *) @@ -685,10 +679,9 @@ let print_extraction_inline () = (* Reset part *) let reset_inline : unit -> obj = - declare_object - {(default_object "Reset Extraction Inline") with - cache_function = (fun (_,_)-> inline_table := empty_inline_table); - load_function = (fun _ (_,_)-> inline_table := empty_inline_table)} + declare_object @@ superglobal_object_nodischarge "Reset Extraction Inline" + ~cache:(fun (_,_)-> inline_table := empty_inline_table) + ~subst:None let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) @@ -731,13 +724,9 @@ let add_implicits r l = (* Registration of operations for rollback. *) let implicit_extraction : GlobRef.t * int_or_id list -> obj = - declare_object - {(default_object "Extraction Implicit") with - cache_function = (fun (_,(r,l)) -> add_implicits r l); - load_function = (fun _ (_,(r,l)) -> add_implicits r l); - classify_function = (fun o -> Substitute o); - subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l)) - } + declare_object @@ superglobal_object_nodischarge "Extraction Implicit" + ~cache:(fun (_,(r,l)) -> add_implicits r l) + ~subst:(Some (fun (s,(r,l)) -> (fst (subst_global s r), l))) (* Grammar entries. *) @@ -784,12 +773,9 @@ let add_blacklist_entries l = (* Registration of operations for rollback. *) let blacklist_extraction : string list -> obj = - declare_object - {(default_object "Extraction Blacklist") with - cache_function = (fun (_,l) -> add_blacklist_entries l); - load_function = (fun _ (_,l) -> add_blacklist_entries l); - subst_function = (fun (_,x) -> x) - } + declare_object @@ superglobal_object_nodischarge "Extraction Blacklist" + ~cache:(fun (_,l) -> add_blacklist_entries l) + ~subst:None (* Grammar entries. *) @@ -805,10 +791,9 @@ let print_extraction_blacklist () = (* Reset part *) let reset_blacklist : unit -> obj = - declare_object - {(default_object "Reset Extraction Blacklist") with - cache_function = (fun (_,_)-> blacklist_table := Id.Set.empty); - load_function = (fun _ (_,_)-> blacklist_table := Id.Set.empty)} + declare_object @@ superglobal_object_nodischarge "Reset Extraction Blacklist" + ~cache:(fun (_,_)-> blacklist_table := Id.Set.empty) + ~subst:None let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ()) @@ -852,23 +837,14 @@ let find_custom_match pv = (* Registration of operations for rollback. *) let in_customs : GlobRef.t * string list * string -> obj = - declare_object - {(default_object "ML extractions") with - cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); - load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); - classify_function = (fun o -> Substitute o); - subst_function = - (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) - } + declare_object @@ superglobal_object_nodischarge "ML extractions" + ~cache:(fun (_,(r,ids,s)) -> add_custom r ids s) + ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))) let in_custom_matchs : GlobRef.t * string -> obj = - declare_object - {(default_object "ML extractions custom matchs") with - cache_function = (fun (_,(r,s)) -> add_custom_match r s); - load_function = (fun _ (_,(r,s)) -> add_custom_match r s); - classify_function = (fun o -> Substitute o); - subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s)) - } + declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs" + ~cache:(fun (_,(r,s)) -> add_custom_match r s) + ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s))) (* Grammar entries. *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 19f954c10d..5d0d17ee6b 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -237,7 +237,6 @@ let cache_Function (_,finfos) = from_graph := Indmap.add finfos.graph_ind finfos !from_graph -let load_Function _ = cache_Function let subst_Function (subst,finfos) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst_ind i = Mod_subst.subst_ind subst i @@ -271,9 +270,6 @@ let subst_Function (subst,finfos) = is_general = finfos.is_general } -let classify_Function infos = Libobject.Substitute infos - - let discharge_Function (_,finfos) = Some finfos let pr_ocst c = @@ -302,15 +298,11 @@ let pr_table tb = Pp.prlist_with_sep fnl pr_info l let in_Function : function_info -> Libobject.obj = - Libobject.declare_object - {(Libobject.default_object "FUNCTIONS_DB") with - Libobject.cache_function = cache_Function; - Libobject.load_function = load_Function; - Libobject.classify_function = classify_Function; - Libobject.subst_function = subst_Function; - Libobject.discharge_function = discharge_Function -(* Libobject.open_function = open_Function; *) - } + let open Libobject in + declare_object @@ superglobal_object "FUNCTIONS_DB" + ~cache:cache_Function + ~subst:(Some subst_Function) + ~discharge:discharge_Function let find_or_none id = diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index ec2adf065a..47f593ff3e 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -531,11 +531,9 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) let inTransitivity : bool * Constr.t -> obj = - declare_object {(default_object "TRANSITIVITY-STEPS") with - cache_function = cache_transitivity_lemma; - open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); - subst_function = subst_transitivity_lemma; - classify_function = (fun o -> Substitute o) } + declare_object @@ global_object_nodischarge "TRANSITIVITY-STEPS" + ~cache:cache_transitivity_lemma + ~subst:(Some subst_transitivity_lemma) (* Main entry points *) diff --git a/plugins/rtauto/g_rtauto.mlg b/plugins/rtauto/g_rtauto.mlg index 9c9fdcfa2f..d8724eb976 100644 --- a/plugins/rtauto/g_rtauto.mlg +++ b/plugins/rtauto/g_rtauto.mlg @@ -17,6 +17,6 @@ open Ltac_plugin DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto -| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) } +| [ "rtauto" ] -> { Refl_tauto.rtauto_tac } END diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index f1fa694356..a6b6c57ff9 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -16,7 +16,6 @@ open CErrors open Util open Term open Constr -open Tacmach open Proof_search open Context.Named.Declaration @@ -60,12 +59,11 @@ let l_I_Or_r = gen_constant "plugins.rtauto.I_Or_r" let l_E_Or = gen_constant "plugins.rtauto.E_Or" let l_D_Or = gen_constant "plugins.rtauto.D_Or" +let special_whd env sigma c = + Reductionops.clos_whd_flags CClosure.all env sigma c -let special_whd gl c = - Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c - -let special_nf gl c = - Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c +let special_nf env sigma c = + Reductionops.clos_norm_flags CClosure.betaiotazeta env sigma c type atom_env= {mutable next:int; @@ -83,61 +81,58 @@ let make_atom atom_env term= atom_env.next<- i + 1; Atom i -let rec make_form atom_env gls term = +let rec make_form env sigma atom_env term = let open EConstr in let open Vars in - let normalize=special_nf gls in - let cciterm=special_whd gls term in - let sigma = Tacmach.project gls in - match EConstr.kind sigma cciterm with - Prod(_,a,b) -> - if noccurn sigma 1 b && - Retyping.get_sort_family_of - (pf_env gls) sigma a == InProp - then - let fa=make_form atom_env gls a in - let fb=make_form atom_env gls b in - Arrow (fa,fb) - else - make_atom atom_env (normalize term) - | Cast(a,_,_) -> - make_form atom_env gls a - | Ind (ind, _) -> - if Names.eq_ind ind (fst (Lazy.force li_False)) then - Bot - else - make_atom atom_env (normalize term) - | App(hd,argv) when Int.equal (Array.length argv) 2 -> - begin - try - let ind, _ = destInd sigma hd in - if Names.eq_ind ind (fst (Lazy.force li_and)) then - let fa=make_form atom_env gls argv.(0) in - let fb=make_form atom_env gls argv.(1) in - Conjunct (fa,fb) - else if Names.eq_ind ind (fst (Lazy.force li_or)) then - let fa=make_form atom_env gls argv.(0) in - let fb=make_form atom_env gls argv.(1) in - Disjunct (fa,fb) - else make_atom atom_env (normalize term) - with DestKO -> make_atom atom_env (normalize term) - end - | _ -> make_atom atom_env (normalize term) - -let rec make_hyps atom_env gls lenv = function + let normalize = special_nf env sigma in + let cciterm = special_whd env sigma term in + match EConstr.kind sigma cciterm with + Prod(_,a,b) -> + if noccurn sigma 1 b && + Retyping.get_sort_family_of env sigma a == InProp + then + let fa = make_form env sigma atom_env a in + let fb = make_form env sigma atom_env b in + Arrow (fa,fb) + else + make_atom atom_env (normalize term) + | Cast(a,_,_) -> + make_form env sigma atom_env a + | Ind (ind, _) -> + if Names.eq_ind ind (fst (Lazy.force li_False)) then + Bot + else + make_atom atom_env (normalize term) + | App(hd,argv) when Int.equal (Array.length argv) 2 -> + begin + try + let ind, _ = destInd sigma hd in + if Names.eq_ind ind (fst (Lazy.force li_and)) then + let fa = make_form env sigma atom_env argv.(0) in + let fb = make_form env sigma atom_env argv.(1) in + Conjunct (fa,fb) + else if Names.eq_ind ind (fst (Lazy.force li_or)) then + let fa = make_form env sigma atom_env argv.(0) in + let fb = make_form env sigma atom_env argv.(1) in + Disjunct (fa,fb) + else make_atom atom_env (normalize term) + with DestKO -> make_atom atom_env (normalize term) + end + | _ -> make_atom atom_env (normalize term) + +let rec make_hyps env sigma atom_env lenv = function [] -> [] | LocalDef (_,body,typ)::rest -> - make_hyps atom_env gls (typ::body::lenv) rest + make_hyps env sigma atom_env (typ::body::lenv) rest | LocalAssum (id,typ)::rest -> - let hrec= - make_hyps atom_env gls (typ::lenv) rest in - if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv || - (Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) typ != InProp) - then - hrec - else - (id,make_form atom_env gls typ)::hrec + let hrec= + make_hyps env sigma atom_env (typ::lenv) rest in + if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv || + (Retyping.get_sort_family_of env sigma typ != InProp) + then + hrec + else + (id,make_form env sigma atom_env typ)::hrec let rec build_pos n = if n<=1 then force node_count l_xH @@ -251,73 +246,76 @@ let () = declare_bool_option opt_check open Pp -let rtauto_tac gls= - Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; - let gamma={next=1;env=[]} in - let gl=pf_concl gls in - let () = - if Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) gl != InProp - then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in - let glf=make_form gamma gls gl in - let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in - let formula= - List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in - let search_fun = match Tacinterp.get_debug() with - | Tactic_debug.DebugOn 0 -> Search.debug_depth_first - | _ -> Search.depth_first - in - let () = - begin - reset_info (); +let rtauto_tac = + Proofview.Goal.enter begin fun gl -> + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; + let gamma={next=1;env=[]} in + let () = + if Retyping.get_sort_family_of env sigma concl != InProp + then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in + let glf = make_form env sigma gamma concl in + let hyps = make_hyps env sigma gamma [concl] hyps in + let formula= + List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in + let search_fun = match Tacinterp.get_debug() with + | Tactic_debug.DebugOn 0 -> Search.debug_depth_first + | _ -> Search.depth_first + in + let () = + begin + reset_info (); + if !verbose then + Feedback.msg_info (str "Starting proof-search ..."); + end in + let search_start_time = System.get_time () in + let prf = + try project (search_fun (init_state [] formula)) + with Not_found -> + user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in + let search_end_time = System.get_time () in + let () = if !verbose then + begin + Feedback.msg_info (str "Proof tree found in " ++ + System.fmt_time_difference search_start_time search_end_time); + pp_info (); + Feedback.msg_info (str "Building proof term ... ") + end in + let build_start_time=System.get_time () in + let () = step_count := 0; node_count := 0 in + let main = mkApp (force node_count l_Reflect, + [|build_env gamma; + build_form formula; + build_proof [] 0 prf|]) in + let term= + applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in + let build_end_time=System.get_time () in + let () = if !verbose then + begin + Feedback.msg_info (str "Proof term built in " ++ + System.fmt_time_difference build_start_time build_end_time ++ + fnl () ++ + str "Proof size : " ++ int !step_count ++ + str " steps" ++ fnl () ++ + str "Proof term size : " ++ int (!step_count+ !node_count) ++ + str " nodes (constants)" ++ fnl () ++ + str "Giving proof term to Coq ... ") + end in + let tac_start_time = System.get_time () in + let term = EConstr.of_constr term in + let result= + if !check then + Tactics.exact_check term + else + Tactics.exact_no_check term in + let tac_end_time = System.get_time () in + let () = + if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then - Feedback.msg_info (str "Starting proof-search ..."); - end in - let search_start_time = System.get_time () in - let prf = - try project (search_fun (init_state [] formula)) - with Not_found -> - user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in - let search_end_time = System.get_time () in - let () = if !verbose then - begin - Feedback.msg_info (str "Proof tree found in " ++ - System.fmt_time_difference search_start_time search_end_time); - pp_info (); - Feedback.msg_info (str "Building proof term ... ") - end in - let build_start_time=System.get_time () in - let () = step_count := 0; node_count := 0 in - let main = mkApp (force node_count l_Reflect, - [|build_env gamma; - build_form formula; - build_proof [] 0 prf|]) in - let term= - applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in - let build_end_time=System.get_time () in - let () = if !verbose then - begin - Feedback.msg_info (str "Proof term built in " ++ - System.fmt_time_difference build_start_time build_end_time ++ - fnl () ++ - str "Proof size : " ++ int !step_count ++ - str " steps" ++ fnl () ++ - str "Proof term size : " ++ int (!step_count+ !node_count) ++ - str " nodes (constants)" ++ fnl () ++ - str "Giving proof term to Coq ... ") - end in - let tac_start_time = System.get_time () in - let term = EConstr.of_constr term in - let result= - if !check then - Proofview.V82.of_tactic (Tactics.exact_check term) gls - else - Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in - let tac_end_time = System.get_time () in - let () = - if !check then Feedback.msg_info (str "Proof term type-checking is on"); - if !verbose then - Feedback.msg_info (str "Internal tactic executed in " ++ - System.fmt_time_difference tac_start_time tac_end_time) in + Feedback.msg_info (str "Internal tactic executed in " ++ + System.fmt_time_difference tac_start_time tac_end_time) in result - + end diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index a91dd666a6..49b5ee5ac7 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -14,14 +14,15 @@ type atom_env= {mutable next:int; mutable env:(Constr.t*int) list} -val make_form : atom_env -> - Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form +val make_form + : Environ.env -> Evd.evar_map -> atom_env + -> EConstr.types -> Proof_search.form -val make_hyps : - atom_env -> - Goal.goal Evd.sigma -> - EConstr.types list -> - EConstr.named_context -> - (Names.Id.t * Proof_search.form) list +val make_hyps + : Environ.env -> Evd.evar_map + -> atom_env + -> EConstr.types list + -> EConstr.named_context + -> (Names.Id.t * Proof_search.form) list -val rtauto_tac : Tacmach.tactic +val rtauto_tac : unit Proofview.tactic diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9fea3ddcda..65201d922f 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -394,13 +394,9 @@ let subst_th (subst,th) = let theory_to_obj : ring_info -> obj = let cache_th (name,th) = add_entry name th in - declare_object - {(default_object "tactic-new-ring-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x)} - + declare_object @@ global_object_nodischarge "tactic-new-ring-theory" + ~cache:cache_th + ~subst:(Some subst_th) let setoid_of_relation env evd a r = try @@ -891,12 +887,9 @@ let subst_th (subst,th) = let ftheory_to_obj : field_info -> obj = let cache_th (name,th) = add_field_entry name th in - declare_object - {(default_object "tactic-new-field-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x) } + declare_object @@ global_object_nodischarge "tactic-new-field-theory" + ~cache:cache_th + ~subst:(Some subst_th) let field_equality evd r inv req = match EConstr.kind !evd req with diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 3f974ea063..1aa64d7141 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -45,16 +45,11 @@ module AdaptorDb = struct let t' = Detyping.subst_glob_constr subst t in if t' == t then a else k, t' - let classify_adaptor x = Libobject.Substitute x - let in_db = - Libobject.declare_object { - (Libobject.default_object "VIEW_ADAPTOR_DB") - with - Libobject.open_function = (fun i o -> if i = 1 then cache_adaptor o); - Libobject.cache_function = cache_adaptor; - Libobject.subst_function = subst_adaptor; - Libobject.classify_function = classify_adaptor } + let open Libobject in + declare_object @@ global_object_nodischarge "VIEW_ADAPTOR_DB" + ~cache:cache_adaptor + ~subst:(Some subst_adaptor) let declare kind terms = List.iter (fun term -> Lib.add_anonymous_leaf (in_db (kind,term))) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f8e8fa9eb9..9c9877fd23 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -69,11 +69,9 @@ let subst_reduction_effect (subst,(con,funkey)) = (subst_constant subst con,funkey) let inReductionEffect : Constant.t * string -> obj = - declare_object {(default_object "REDUCTION-EFFECT") with - cache_function = cache_reduction_effect; - open_function = (fun i o -> if Int.equal i 1 then cache_reduction_effect o); - subst_function = subst_reduction_effect; - classify_function = (fun o -> Substitute o) } + declare_object @@ global_object_nodischarge "REDUCTION-EFFECT" + ~cache:cache_reduction_effect + ~subst:(Some subst_reduction_effect) let declare_reduction_effect funkey f = if String.Map.mem funkey !effect_table then diff --git a/printing/printer.ml b/printing/printer.ml index 83f1f8d8e9..b80133b171 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -722,11 +722,11 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map let get_ogs g = match os_map with | Some (osigma, _) -> - (* if Not_found, returning None treats the goal as new and it will be highlighted; + (* if Not_found, returning None treats the goal as new and it will be diff highlighted; returning Some { it = g; sigma = sigma } will compare the new goal to itself and it won't be highlighted *) (try Some { it = GoalMap.find g diff_goal_map; sigma = osigma } - with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (7)")) + with Not_found -> None) | None -> None in let rec pr_rec n = function diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 3e2093db4a..a381266976 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -83,7 +83,7 @@ let tokenize_string s = if Tok.(equal e EOI) then List.rev acc else - stream_tok ((Tok.extract_string e) :: acc) str + stream_tok ((Tok.extract_string true e) :: acc) str in let st = CLexer.get_lexer_state () in try @@ -138,13 +138,11 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = let hyp_diffs = diff_str ~tokenize_string o_line n_line in let (has_added, has_removed) = has_changes hyp_diffs in if show_removed () && has_removed then begin - let o_entry = StringMap.find (List.hd old_ids) o_map in - o_entry.done_ <- true; + List.iter (fun x -> (StringMap.find x o_map).done_ <- true) old_ids; rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv; end; if n_line <> "" then begin - let n_entry = StringMap.find (List.hd new_ids) n_map in - n_entry.done_ <- true; + List.iter (fun x -> (StringMap.find x n_map).done_ <- true) new_ids; rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv end in @@ -157,7 +155,7 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = if dtype = `Removed then begin let o_idents = (StringMap.find ident o_map).idents in (* only show lines that have all idents removed here; other removed idents appear later *) - if show_removed () && + if show_removed () && not (is_done ident o_map) && List.for_all (fun x -> not (exists x n_map)) o_idents then output (List.rev o_idents) [] end @@ -399,6 +397,10 @@ let match_goals ot nt = It's set to the old goal's evar name once a rewitten goal is found, at which point the code only searches for the replacing goals (and ot is set to nt). *) + let iter2 f l1 l2 = + if List.length l1 = (List.length l2) then + List.iter2 f l1 l2 + in let rec match_goals_r ogname ot nt = let constr_expr ogname exp exp2 = match_goals_r ogname exp.v exp2.v @@ -434,13 +436,13 @@ let match_goals ot nt = let fix_expr ogname exp exp2 = let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in recursion_order_expr ogname ro ro2; - List.iter2 (local_binder_expr ogname) lb lb2; + iter2 (local_binder_expr ogname) lb lb2; constr_expr ogname ce1 ce12; constr_expr ogname ce2 ce22 in let cofix_expr ogname exp exp2 = let (l,lb,ce1,ce2), (l2,lb2,ce12,ce22) = exp,exp2 in - List.iter2 (local_binder_expr ogname) lb lb2; + iter2 (local_binder_expr ogname) lb lb2; constr_expr ogname ce1 ce12; constr_expr ogname ce2 ce22 in @@ -454,38 +456,38 @@ let match_goals ot nt = in let constr_notation_substitution ogname exp exp2 = let (ce, cel, cp, lb), (ce2, cel2, cp2, lb2) = exp, exp2 in - List.iter2 (constr_expr ogname) ce ce2; - List.iter2 (fun a a2 -> List.iter2 (constr_expr ogname) a a2) cel cel2; - List.iter2 (fun a a2 -> List.iter2 (local_binder_expr ogname) a a2) lb lb2 + iter2 (constr_expr ogname) ce ce2; + iter2 (fun a a2 -> iter2 (constr_expr ogname) a a2) cel cel2; + iter2 (fun a a2 -> iter2 (local_binder_expr ogname) a a2) lb lb2 in begin match ot, nt with | CRef (ref,us), CRef (ref2,us2) -> () | CFix (id,fl), CFix (id2,fl2) -> - List.iter2 (fix_expr ogname) fl fl2 + iter2 (fix_expr ogname) fl fl2 | CCoFix (id,cfl), CCoFix (id2,cfl2) -> - List.iter2 (cofix_expr ogname) cfl cfl2 + iter2 (cofix_expr ogname) cfl cfl2 | CProdN (bl,c2), CProdN (bl2,c22) | CLambdaN (bl,c2), CLambdaN (bl2,c22) -> - List.iter2 (local_binder_expr ogname) bl bl2; + iter2 (local_binder_expr ogname) bl bl2; constr_expr ogname c2 c22 | CLetIn (na,c1,t,c2), CLetIn (na2,c12,t2,c22) -> constr_expr ogname c1 c12; constr_expr_opt ogname t t2; constr_expr ogname c2 c22 | CAppExpl ((isproj,ref,us),args), CAppExpl ((isproj2,ref2,us2),args2) -> - List.iter2 (constr_expr ogname) args args2 + iter2 (constr_expr ogname) args args2 | CApp ((isproj,f),args), CApp ((isproj2,f2),args2) -> constr_expr ogname f f2; - List.iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in + iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in constr_expr ogname c c2) args args2 | CRecord fs, CRecord fs2 -> - List.iter2 (fun a a2 -> let (_, c) = a and (_, c2) = a2 in + iter2 (fun a a2 -> let (_, c) = a and (_, c2) = a2 in constr_expr ogname c c2) fs fs2 | CCases (sty,rtnpo,tms,eqns), CCases (sty2,rtnpo2,tms2,eqns2) -> constr_expr_opt ogname rtnpo rtnpo2; - List.iter2 (case_expr ogname) tms tms2; - List.iter2 (branch_expr ogname) eqns eqns2 + iter2 (case_expr ogname) tms tms2; + iter2 (branch_expr ogname) eqns eqns2 | CLetTuple (nal,(na,po),b,c), CLetTuple (nal2,(na2,po2),b2,c2) -> constr_expr_opt ogname po po2; constr_expr ogname b b2; @@ -500,7 +502,7 @@ let match_goals ot nt = | CEvar (n,l), CEvar (n2,l2) -> let oevar = if ogname = "" then Id.to_string n else ogname in nevar_to_oevar := StringMap.add (Id.to_string n2) oevar !nevar_to_oevar; - List.iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 + iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 | CEvar (n,l), nt' -> (* pass down the old goal evar name *) match_goals_r (Id.to_string n) nt' nt' @@ -545,19 +547,31 @@ module GoalMap = Evar.Map let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma) +open Goal.Set + [@@@ocaml.warning "-32"] let db_goal_map op np ng_to_og = - Printf.printf "New Goals: "; - let (ngoals,_,_,_,nsigma) = Proof.proof np in - List.iter (fun ng -> Printf.printf "%d -> %s " (Evar.repr ng) (goal_to_evar ng nsigma)) ngoals; + let pr_goals title prf = + Printf.printf "%s: " title; + let (goals,_,_,_,sigma) = Proof.proof prf in + List.iter (fun g -> Printf.printf "%d -> %s " (Evar.repr g) (goal_to_evar g sigma)) goals; + let gs = diff (Proof.all_goals prf) (List.fold_left (fun s g -> add g s) empty goals) in + List.iter (fun g -> Printf.printf "%d " (Evar.repr g)) (elements gs); + in + + pr_goals "New Goals" np; (match op with | Some op -> - let (ogoals,_,_,_,osigma) = Proof.proof op in - Printf.printf "\nOld Goals: "; - List.iter (fun og -> Printf.printf "%d -> %s " (Evar.repr og) (goal_to_evar og osigma)) ogoals + pr_goals "\nOld Goals" op | None -> ()); Printf.printf "\nGoal map: "; - GoalMap.iter (fun og ng -> Printf.printf "%d -> %d " (Evar.repr og) (Evar.repr ng)) ng_to_og; + GoalMap.iter (fun ng og -> Printf.printf "%d -> %d " (Evar.repr ng) (Evar.repr og)) ng_to_og; + let unmapped = ref (Proof.all_goals np) in + GoalMap.iter (fun ng _ -> unmapped := Goal.Set.remove ng !unmapped) ng_to_og; + if Goal.Set.cardinal !unmapped > 0 then begin + Printf.printf "\nUnmapped goals: "; + Goal.Set.iter (fun ng -> Printf.printf "%d " (Evar.repr ng)) !unmapped + end; Printf.printf "\n" [@@@ocaml.warning "+32"] diff --git a/tactics/auto.ml b/tactics/auto.ml index c030c77d4d..f5c3619e64 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -211,30 +211,26 @@ let tclLOG (dbg,_,depth,trace) pp tac = match dbg with | Off -> tac | Debug -> - (* For "debug (trivial/auto)", we directly output messages *) + (* For "debug (trivial/auto)", we directly output messages *) let s = String.make (depth+1) '*' in - Proofview.V82.tactic begin fun gl -> - try - let out = Proofview.V82.of_tactic tac gl in - Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); - out - with reraise -> - let reraise = CErrors.push reraise in - Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); - iraise reraise - end + Proofview.(tclIFCATCH ( + tac >>= fun v -> + Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); + tclUNIT v + ) Proofview.tclUNIT + (fun (exn, info) -> + Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); + tclZERO ~info exn)) | Info -> (* For "info (trivial/auto)", we store a log trace *) - Proofview.V82.tactic begin fun gl -> - try - let out = Proofview.V82.of_tactic tac gl in - trace := (depth, Some pp) :: !trace; - out - with reraise -> - let reraise = CErrors.push reraise in - trace := (depth, None) :: !trace; - iraise reraise - end + Proofview.(tclIFCATCH ( + tac >>= fun v -> + trace := (depth, Some pp) :: !trace; + tclUNIT v + ) Proofview.tclUNIT + (fun (exn, info) -> + trace := (depth, None) :: !trace; + tclZERO ~info exn)) (** For info, from the linear trace information, we reconstitute the part of the proof tree we're interested in. The last executed tactic diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 76cbdee0d5..f824552705 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -196,17 +196,12 @@ let subst_hintrewrite (subst,(rbase,list as node)) = if list' == list then node else (rbase,list') -let classify_hintrewrite x = Libobject.Substitute x - - (* Declaration of the Hint Rewrite library object *) let inHintRewrite : string * HintDN.t -> Libobject.obj = - Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with - Libobject.cache_function = cache_hintrewrite; - Libobject.load_function = (fun _ -> cache_hintrewrite); - Libobject.subst_function = subst_hintrewrite; - Libobject.classify_function = classify_hintrewrite } - + let open Libobject in + declare_object @@ superglobal_object_nodischarge "HINT_REWRITE" + ~cache:cache_hintrewrite + ~subst:(Some subst_hintrewrite) open Clenv diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index a53e3bf20d..a67f5f6d6e 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -59,12 +59,10 @@ let discharge_scheme (_,(kind,l)) = Some (kind, l) let inScheme : string * (inductive * Constant.t) array -> obj = - declare_object {(default_object "SCHEME") with - cache_function = cache_scheme; - load_function = (fun _ -> cache_scheme); - subst_function = subst_scheme; - classify_function = (fun obj -> Substitute obj); - discharge_function = discharge_scheme} + declare_object @@ superglobal_object "SCHEME" + ~cache:cache_scheme + ~subst:(Some subst_scheme) + ~discharge:discharge_scheme (**********************************************************************) (* The table of scheme building functions *) diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v new file mode 100644 index 0000000000..8a7e9c37b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_9166.v @@ -0,0 +1,9 @@ +Set Warnings "+deprecated". + +Notation bar := option (compat "8.7"). + +Definition foo (x: nat) : nat := + match x with + | 0 => 0 + | S bar => bar + end. diff --git a/theories/Strings/BinaryString.v b/theories/Strings/BinaryString.v index 6df0a9170a..a2bb1763f5 100644 --- a/theories/Strings/BinaryString.v +++ b/theories/Strings/BinaryString.v @@ -48,7 +48,7 @@ Module Raw. end end. - Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) + Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} : to_N (of_pos p rest) base = to_N rest match base with | N0 => N.pos p diff --git a/theories/Strings/HexString.v b/theories/Strings/HexString.v index 9ea93c909e..9fa8e0ccf2 100644 --- a/theories/Strings/HexString.v +++ b/theories/Strings/HexString.v @@ -120,7 +120,7 @@ Module Raw. end end. - Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) + Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} : to_N (of_pos p rest) base = to_N rest match base with | N0 => N.pos p diff --git a/theories/Strings/OctalString.v b/theories/Strings/OctalString.v index fe8cc9aae9..78e98e451b 100644 --- a/theories/Strings/OctalString.v +++ b/theories/Strings/OctalString.v @@ -78,7 +78,7 @@ Module Raw. end end. - Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) + Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} : to_N (of_pos p rest) base = to_N rest match base with | N0 => N.pos p diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index dccd776fa8..790b62c9d0 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -33,11 +33,9 @@ open Nameops let cache_token (_,s) = CLexer.add_keyword s let inToken : string -> obj = - declare_object {(default_object "TOKEN") with - open_function = (fun i o -> if Int.equal i 1 then cache_token o); - cache_function = cache_token; - subst_function = Libobject.ident_subst_function; - classify_function = (fun o -> Substitute o)} + declare_object @@ global_object_nodischarge "TOKEN" + ~cache:cache_token + ~subst:(Some Libobject.ident_subst_function) let add_token_obj s = Lib.add_anonymous_leaf (inToken s) |