diff options
67 files changed, 379 insertions, 293 deletions
diff --git a/Makefile.dev b/Makefile.dev index 1803cc8ff..fde92ec94 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -98,7 +98,7 @@ pluginsopt: $(PLUGINSOPT) pluginsbyte: $(PLUGINS) # This should build all the ocaml code but not (most of) the .v files -coqocaml: tools coqbinaries pluginsopt coqide printers +coqocaml: tools coqbinaries pluginsopt coqide printers bin/votour .PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml diff --git a/checker/analyze.ml b/checker/analyze.ml index c48b83011..df75d5b93 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -4,6 +4,7 @@ let prefix_small_block = 0x80 let prefix_small_int = 0x40 let prefix_small_string = 0x20 +[@@@ocaml.warning "-32"] let code_int8 = 0x00 let code_int16 = 0x01 let code_int32 = 0x02 @@ -25,6 +26,7 @@ let code_infixpointer = 0x11 let code_custom = 0x12 let code_block64 = 0x13 +[@@@ocaml.warning "-37"] type code_descr = | CODE_INT8 | CODE_INT16 @@ -101,11 +103,11 @@ let input_binary_int chan = input_binary_int chan let input_char chan = Char.chr (input_byte chan) +let input_string len chan = String.init len (fun _ -> input_char chan) let parse_header chan = let () = current_offset := 0 in - let magic = String.create 4 in - let () = for i = 0 to 3 do magic.[i] <- input_char chan done in + let magic = input_string 4 chan in let length = input_binary_int chan in let objects = input_binary_int chan in let size32 = input_binary_int chan in @@ -204,13 +206,6 @@ let input_header64 chan = in (tag, len) -let input_string len chan = - let ans = String.create len in - for i = 0 to pred len do - ans.[i] <- input_char chan; - done; - ans - let parse_object chan = let data = input_byte chan in if prefix_small_block <= data then @@ -251,7 +246,7 @@ let parse_object chan = RString (input_string len chan) | CODE_CODEPOINTER -> let addr = input_int32u chan in - for i = 0 to 15 do ignore (input_byte chan); done; + for _i = 0 to 15 do ignore (input_byte chan); done; RCode addr | CODE_DOUBLE_ARRAY32_LITTLE | CODE_DOUBLE_BIG diff --git a/checker/votour.ml b/checker/votour.ml index 48f9f45e7..c255e5cdb 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -19,14 +19,14 @@ let rec read_num max = if l = "u" then None else if l = "x" then quit () else - try - let v = int_of_string l in + match int_of_string l with + | v -> if v < 0 || v >= max then let () = Printf.printf "Out-of-range input! (only %d children)\n%!" max in read_num max else Some v - with Failure "int_of_string" -> + | exception Failure _ -> Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!"; read_num max @@ -149,16 +149,17 @@ let rec get_name ?(extra=false) = function (** For tuples, its quite handy to display the inner 1st string (if any). Cf. [structure_body] for instance *) +exception TupleString of string let get_string_in_tuple o = try for i = 0 to Array.length o - 1 do match Repr.repr o.(i) with | STRING s -> - failwith (Printf.sprintf " [..%s..]" s) + raise (TupleString (Printf.sprintf " [..%s..]" s)) | _ -> () done; "" - with Failure s -> s + with TupleString s -> s (** Some details : tags, integer value for non-block, etc etc *) @@ -205,6 +206,7 @@ let access_block o = match Repr.repr o with let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit (** raises Exit if the object has not the expected structure *) +exception Forbidden let rec get_children v o pos = match v with |Tuple (_, v) -> let (_, os) = access_block o in @@ -236,7 +238,7 @@ let rec get_children v o pos = match v with [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|] | _ -> raise Exit end - |Fail s -> failwith "forbidden" + |Fail s -> raise Forbidden let get_children v o pos = try get_children v o pos @@ -257,9 +259,10 @@ let init () = stk := [] let push name v o p = stk := { nam = name; typ = v; obj = o; pos = p } :: !stk +exception EmptyStack let pop () = match !stk with | i::s -> stk := s; i - | _ -> failwith "empty stack" + | _ -> raise EmptyStack let rec visit v o pos = Printf.printf "\nDepth %d Pos %s Context %s\n" @@ -283,8 +286,8 @@ let rec visit v o pos = push (get_name v) v o pos; visit v' o' pos' with - | Failure "empty stack" -> () - | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos + | EmptyStack -> () + | Forbidden -> let info = pop () in visit info.typ info.obj info.pos | Failure _ | Invalid_argument _ -> visit v o pos end @@ -313,8 +316,7 @@ let dummy_header = { } let parse_header chan = - let magic = String.create 4 in - let () = for i = 0 to 3 do magic.[i] <- input_char chan done in + let magic = really_input_string chan 4 in let length = input_binary_int chan in let objects = input_binary_int chan in let size32 = input_binary_int chan in diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 1f7fbcbf6..bfa43cde1 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,8 +25,10 @@ echo $TRAVIS_PULL_REQUEST echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT -if [ $TRAVIS_PULL_REQUEST == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then - mathcomp_CI_BRANCH=options+remove_non_sync +if [ $TRAVIS_PULL_REQUEST == "678" ] || [ $TRAVIS_BRANCH == "coqlib-part-02" ]; then + + mathcomp_CI_BRANCH=coqlib-part-02 mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git + fi diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 0b0c0f5bf..7fad65bf0 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -108,6 +108,19 @@ In GOption: passed to workers, etc... As a consequence, the field `Goptions.optsync` has been removed. +In Coqlib / reference location: + + We have removed from Coqlib functions returning `constr` from + names. Now it is only possible to obtain references, that must be + processed wrt the particular needs of the client. + + Users of `coq_constant/gen_constant` can do + `Universes.constr_of_global (find_reference dir r)` _however_ note + the warnings in the `Universes.constr_of_global` in the + documentation. It is very likely that you were previously suffering + from problems with polymorphic universes due to using + `Coqlib.coq_constant` that used to do this. + ** Tactic API ** - pf_constr_of_global now returns a tactic instead of taking a continuation. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 0346c4a55..bb679ecba 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -522,6 +522,19 @@ to have \emph{at least} one success. \ErrMsg \errindex{No applicable tactic} +\variant {\tt first {\tacexpr}} + +This is an Ltac alias that gives a primitive access to the {\tt first} tactical +as a Ltac definition without going through a parsing rule. It expects to be +given a list of tactics through a {\tt Tactic Notation}, allowing to write +notations of the following form. + +\Example + +\begin{quote} +{\tt Tactic Notation "{foo}" tactic\_list(tacs) := first tacs.} +\end{quote} + \subsubsection[Left-biased branching]{Left-biased branching\tacindex{$\mid\mid$} \index{Tacticals!orelse@{\tt $\mid\mid$}}} @@ -600,6 +613,11 @@ $v_2$ and so on. It fails if there is no solving tactic. \ErrMsg \errindex{Cannot solve the goal} +\variant {\tt solve {\tacexpr}} + +This is an Ltac alias that gives a primitive access to the {\tt solve} tactical. +See the {\tt first} tactical for more information. + \subsubsection[Identity]{Identity\label{ltac:idtac}\tacindex{idtac} \index{Tacticals!idtac@{\tt idtac}}} diff --git a/engine/termops.ml b/engine/termops.ml index 19e62f8e6..ca32c06a7 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1468,25 +1468,3 @@ let env_rel_context_chop k env = let ctx1,ctx2 = List.chop k rels in push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), ctx1 - -(*******************************************) -(* Functions to deal with impossible cases *) -(*******************************************) -let impossible_default_case = ref None - -let set_impossible_default_clause c = impossible_default_case := Some c - -let coq_unit_judge = - let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in - let na1 = Name (Id.of_string "A") in - let na2 = Name (Id.of_string "H") in - fun () -> - match !impossible_default_case with - | Some fn -> - let (id,type_of_id), ctx = fn () in - make_judge id type_of_id, ctx - | None -> - (* In case the constants id/ID are not defined *) - make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) - (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), - Univ.ContextSet.empty diff --git a/engine/termops.mli b/engine/termops.mli index fe6dfb0ce..58837ba03 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -275,10 +275,6 @@ val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) puns val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment -(** {6 Functions to deal with impossible cases } *) -val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit -val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set - (** {5 Debug pretty-printers} *) open Evd diff --git a/interp/interp.mllib b/interp/interp.mllib index 607af82a0..6d290a325 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -14,6 +14,5 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Coqlib Discharge Declare diff --git a/interp/coqlib.ml b/library/coqlib.ml index 9539980f0..955ff4c08 100644 --- a/interp/coqlib.ml +++ b/library/coqlib.ml @@ -10,11 +10,9 @@ open CErrors open Util open Pp open Names -open Term open Libnames open Globnames open Nametab -open Smartlocate let coq = Nameops.coq_string (* "Coq" *) @@ -26,29 +24,27 @@ type message = string let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = - let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in - try global_of_extended_global (Nametab.extended_global_of_path sp) + let dp = make_dir dir in + let sp = Libnames.make_path dp (Id.of_string s) in + try Nametab.global_of_path sp with Not_found -> - anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp) + (* Following bug 5066 we are more permissive with the handling + of not found errors here *) + user_err ~hdr:locstr + Pp.(str "cannot find " ++ Libnames.pr_path sp ++ + str "; maybe library " ++ Libnames.pr_dirpath dp ++ + str " has to be required first.") let coq_reference locstr dir s = find_reference locstr (coq::dir) s -let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) - -let gen_reference = coq_reference -let gen_constant = coq_constant let has_suffix_in_dirs dirs ref = let dir = dirpath (path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs -let global_of_extended q = - try Some (global_of_extended_global q) with Not_found -> None - let gen_reference_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let qualid = qualid_of_string s in - let all = Nametab.locate_extended_all qualid in - let all = List.map_filter global_of_extended all in + let all = Nametab.locate_all qualid in let all = List.sort_uniquize RefOrdered_env.compare all in let these = List.filter (has_suffix_in_dirs dirs) all in match these with @@ -65,10 +61,6 @@ let gen_reference_in_modules locstr dirs s = str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma pr_dirpath dirs) -let gen_constant_in_modules locstr dirs s = - Universes.constr_of_global (gen_reference_in_modules locstr dirs s) - - (* For tactics/commands requiring vernacular libraries *) let check_required_library d = @@ -93,16 +85,12 @@ let check_required_library d = (* Specific Coq objects *) let init_reference dir s = - let d = "Init"::dir in - check_required_library (coq::d); gen_reference "Coqlib" d s - -let init_constant dir s = - let d = "Init"::dir in - check_required_library (coq::d); gen_constant "Coqlib" d s + let d = coq::"Init"::dir in + check_required_library d; find_reference "Coqlib" d s let logic_reference dir s = - let d = "Logic"::dir in - check_required_library ("Coq"::d); gen_reference "Coqlib" d s + let d = coq::"Logic"::dir in + check_required_library d; find_reference "Coqlib" d s let arith_dir = [coq;"Arith"] let arith_modules = [arith_dir] @@ -149,12 +137,6 @@ let make_con dir id = Globnames.encode_con dir (Id.of_string id) let id = make_con datatypes_module "idProp" let type_of_id = make_con datatypes_module "IDProp" -let _ = Termops.set_impossible_default_clause - (fun () -> - let c, ctx = Universes.fresh_global_instance (Global.env()) (ConstRef id) in - let (_, u) = destConst c in - (c,mkConstU (type_of_id,u)), ctx) - (** Natural numbers *) let nat_kn = make_ind datatypes_module "nat" let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat") @@ -194,14 +176,14 @@ type coq_sigma_data = { typ : global_reference } type coq_bool_data = { - andb : constr; - andb_prop : constr; - andb_true_intro : constr} + andb : global_reference; + andb_prop : global_reference; + andb_true_intro : global_reference} let build_bool_type () = - { andb = init_constant ["Datatypes"] "andb"; - andb_prop = init_constant ["Datatypes"] "andb_prop"; - andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" } + { andb = init_reference ["Datatypes"] "andb"; + andb_prop = init_reference ["Datatypes"] "andb_prop"; + andb_true_intro = init_reference ["Datatypes"] "andb_true_intro" } let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type") @@ -244,7 +226,6 @@ type coq_inversion_data = { } let lazy_init_reference dir id = lazy (init_reference dir id) -let lazy_init_constant dir id = lazy (init_constant dir id) let lazy_logic_reference dir id = lazy (logic_reference dir id) (* Leibniz equality on Type *) @@ -307,7 +288,7 @@ let build_coq_inversion_jmeq_data () = inv_congr = Lazy.force coq_jmeq_congr_canonical } (* Specif *) -let coq_sumbool = lazy_init_constant ["Specif"] "sumbool" +let coq_sumbool = lazy_init_reference ["Specif"] "sumbool" let build_coq_sumbool () = Lazy.force coq_sumbool @@ -349,22 +330,22 @@ let build_coq_inversion_eq_true_data () = inv_congr = Lazy.force coq_eq_true_congr } (* The False proposition *) -let coq_False = lazy_init_constant ["Logic"] "False" +let coq_False = lazy_init_reference ["Logic"] "False" (* The True proposition and its unique proof *) -let coq_True = lazy_init_constant ["Logic"] "True" -let coq_I = lazy_init_constant ["Logic"] "I" +let coq_True = lazy_init_reference ["Logic"] "True" +let coq_I = lazy_init_reference ["Logic"] "I" (* Connectives *) -let coq_not = lazy_init_constant ["Logic"] "not" -let coq_and = lazy_init_constant ["Logic"] "and" -let coq_conj = lazy_init_constant ["Logic"] "conj" -let coq_or = lazy_init_constant ["Logic"] "or" -let coq_ex = lazy_init_constant ["Logic"] "ex" -let coq_iff = lazy_init_constant ["Logic"] "iff" +let coq_not = lazy_init_reference ["Logic"] "not" +let coq_and = lazy_init_reference ["Logic"] "and" +let coq_conj = lazy_init_reference ["Logic"] "conj" +let coq_or = lazy_init_reference ["Logic"] "or" +let coq_ex = lazy_init_reference ["Logic"] "ex" +let coq_iff = lazy_init_reference ["Logic"] "iff" -let coq_iff_left_proj = lazy_init_constant ["Logic"] "proj1" -let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2" +let coq_iff_left_proj = lazy_init_reference ["Logic"] "proj1" +let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2" (* Runtime part *) let build_coq_True () = Lazy.force coq_True @@ -385,8 +366,8 @@ let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj (* The following is less readable but does not depend on parsing *) let coq_eq_ref = lazy (init_reference ["Logic"] "eq") let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") -let coq_jmeq_ref = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq") -let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true") +let coq_jmeq_ref = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq") +let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true") let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref")) let coq_existT_ref = lazy (init_reference ["Specif"] "existT") let coq_exist_ref = lazy (init_reference ["Specif"] "exist") @@ -397,3 +378,6 @@ let coq_sig_ref = lazy (init_reference ["Specif"] "sig") let coq_or_ref = lazy (init_reference ["Logic"] "or") let coq_iff_ref = lazy (init_reference ["Logic"] "iff") +(* Deprecated *) +let gen_reference = coq_reference + diff --git a/interp/coqlib.mli b/library/coqlib.mli index 1facb47e1..716d97c9d 100644 --- a/interp/coqlib.mli +++ b/library/coqlib.mli @@ -9,12 +9,30 @@ open Names open Libnames open Globnames -open Term open Util (** This module collects the global references, constructions and patterns of the standard library used in ocaml files *) +(** The idea is to migrate to rebindable name-based approach, thus the + only function this FILE will provide will be: + + [find_reference : string -> global_reference] + + such that [find_reference "core.eq.type"] returns the proper [global_reference] + + [bind_reference : string -> global_reference -> unit] + + will bind a reference. + + A feature based approach would be possible too. + + Contrary to the old approach of raising an anomaly, we expect + tactics to gracefully fail in the absence of some primitive. + + This is work in progress, see below. +*) + (** {6 ... } *) (** [find_reference caller_message [dir;subdir;...] s] returns a global reference to the name dir.subdir.(...).s; the corresponding module @@ -25,31 +43,18 @@ open Util type message = string val find_reference : message -> string list -> string -> global_reference - -(** [coq_reference caller_message [dir;subdir;...] s] returns a - global reference to the name Coq.dir.subdir.(...).s *) - val coq_reference : message -> string list -> string -> global_reference -(** idem but return a term *) - -val coq_constant : message -> string list -> string -> constr - -(** Synonyms of [coq_constant] and [coq_reference] *) - -val gen_constant : message -> string list -> string -> constr -val gen_reference : message -> string list -> string -> global_reference +(** For tactics/commands requiring vernacular libraries *) +val check_required_library : string list -> unit (** Search in several modules (not prefixed by "Coq") *) -val gen_constant_in_modules : string->string list list-> string -> constr val gen_reference_in_modules : string->string list list-> string -> global_reference + val arith_modules : string list list val zarith_base_modules : string list list val init_modules : string list list -(** For tactics/commands requiring vernacular libraries *) -val check_required_library : string list -> unit - (** {6 Global references } *) (** Modules *) @@ -65,6 +70,10 @@ val jmeq_module_name : string list val datatypes_module_name : string list +(** Identity *) +val id : constant +val type_of_id : constant + (** Natural numbers *) val nat_path : full_path val glob_nat : global_reference @@ -95,9 +104,9 @@ val glob_jmeq : global_reference at runtime. *) type coq_bool_data = { - andb : constr; - andb_prop : constr; - andb_true_intro : constr} + andb : global_reference; + andb_prop : global_reference; + andb_true_intro : global_reference} val build_bool_type : coq_bool_data delayed (** {6 For Equality tactics } *) @@ -154,33 +163,33 @@ val build_coq_inversion_jmeq_data : coq_inversion_data delayed val build_coq_inversion_eq_true_data : coq_inversion_data delayed (** Specif *) -val build_coq_sumbool : constr delayed +val build_coq_sumbool : global_reference delayed (** {6 ... } *) (** Connectives The False proposition *) -val build_coq_False : constr delayed +val build_coq_False : global_reference delayed (** The True proposition and its unique proof *) -val build_coq_True : constr delayed -val build_coq_I : constr delayed +val build_coq_True : global_reference delayed +val build_coq_I : global_reference delayed (** Negation *) -val build_coq_not : constr delayed +val build_coq_not : global_reference delayed (** Conjunction *) -val build_coq_and : constr delayed -val build_coq_conj : constr delayed -val build_coq_iff : constr delayed +val build_coq_and : global_reference delayed +val build_coq_conj : global_reference delayed +val build_coq_iff : global_reference delayed -val build_coq_iff_left_proj : constr delayed -val build_coq_iff_right_proj : constr delayed +val build_coq_iff_left_proj : global_reference delayed +val build_coq_iff_right_proj : global_reference delayed (** Disjunction *) -val build_coq_or : constr delayed +val build_coq_or : global_reference delayed (** Existential quantifier *) -val build_coq_ex : constr delayed +val build_coq_ex : global_reference delayed val coq_eq_ref : global_reference lazy_t val coq_identity_ref : global_reference lazy_t @@ -196,3 +205,7 @@ val coq_sig_ref : global_reference lazy_t val coq_or_ref : global_reference lazy_t val coq_iff_ref : global_reference lazy_t + +(* Deprecated functions *) +val gen_reference : message -> string list -> string -> global_reference +[@@ocaml.deprecated "Please use Coqlib.find_reference"] diff --git a/library/library.mllib b/library/library.mllib index df4f73503..6f433b77d 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -16,3 +16,4 @@ Goptions Decls Heads Keys +Coqlib diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index a0b04ce3b..33a9dd4fd 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -8,7 +8,7 @@ let init_constant dir s = in find_constant contrib_name dir s -let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s) +let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 201726d1e..b3017f359 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -26,7 +26,7 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) +let reference dir s = lazy (Coqlib.coq_reference "CC" dir s) let _f_equal = reference ["Init";"Logic"] "f_equal" let _eq_rect = reference ["Init";"Logic"] "eq_rect" diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 86a677007..8c6b5b91d 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -231,7 +231,8 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) -let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str +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"))); diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index f397f84a8..a6290cb00 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -285,14 +285,15 @@ let fourier_lineq lineq1 = let get = Lazy.force let cget = get let eget c = EConstr.of_constr (Lazy.force c) -let constant = Coqlib.gen_constant "Fourier" +let constant path s = Universes.constr_of_global @@ + Coqlib.coq_reference "Fourier" path s (* Standard library *) open Coqlib let coq_sym_eqT = lazy (build_coq_eq_sym ()) -let coq_False = lazy (build_coq_False ()) -let coq_not = lazy (build_coq_not ()) -let coq_eq = lazy (build_coq_eq ()) +let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ()) +let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ()) +let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ()) (* Rdefinitions *) let constant_real = constant ["Reals";"Rdefinitions"] diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 64f7813a3..434fb14a6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -409,9 +409,9 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (Coqlib.build_coq_False ()) in - let coq_True = EConstr.of_constr (Coqlib.build_coq_True ()) in - let coq_I = EConstr.of_constr (Coqlib.build_coq_I ()) in + let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in + let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in + let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in @@ -1596,7 +1596,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ()) + | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index d8614f376..68e097fe9 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -248,10 +248,10 @@ let mk_result ctxt value avoid = **************************************************) let coq_True_ref = - lazy (Coqlib.gen_reference "" ["Init";"Logic"] "True") + lazy (Coqlib.coq_reference "" ["Init";"Logic"] "True") let coq_False_ref = - lazy (Coqlib.gen_reference "" ["Init";"Logic"] "False") + lazy (Coqlib.coq_reference "" ["Init";"Logic"] "False") (* [make_discr_match_el \[e1,...en\]] builds match e1,...,en with diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 91dac303a..2476478ab 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -120,7 +120,8 @@ let def_of_const t = |_ -> assert false let coq_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; let find_reference sl s = @@ -469,13 +470,17 @@ exception ToShow of exn let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; - EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq") + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; - EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl") + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = @@ -486,7 +491,10 @@ let hrec_id = Id.of_string "hrec" let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded") let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") -let well_founded_ltof = function () -> EConstr.of_constr (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof") + +let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@ + Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" + let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8747efc02..d68bdc215 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -546,7 +546,7 @@ and intros_with_rewrite_aux : tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENSEQ[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e206955ac..2f9f70876 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -47,14 +47,16 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) -let coq_constant m s = - EConstr.of_constr (Coqlib.coq_constant "RecursiveDefinition" m s) +let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ + Coqlib.coq_reference "RecursiveDefinition" m s let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["Arith";"Lt"] let coq_init_constant s = - EConstr.of_constr (Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s) + EConstr.of_constr ( + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -1223,7 +1225,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = Coqlib.build_coq_and () in + let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in let conj_constr = coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 6890b3198..0a13a20a9 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -326,3 +326,35 @@ let initial_atomic () = ] let () = Mltop.declare_cache_obj initial_atomic "coretactics" + +(* First-class Ltac access to primitive blocks *) + +let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; } +let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; } + +let register_list_tactical name f = + let tac args ist = match args with + | [v] -> + begin match Tacinterp.Value.to_list v with + | None -> Tacticals.New.tclZEROMSG (Pp.str "Expected a list") + | Some tacs -> + let tacs = List.map (fun tac -> Tacinterp.tactic_of_value ist tac) tacs in + f tacs + end + | _ -> assert false + in + Tacenv.register_ml_tactic (initial_name name) [|tac|] + +let () = register_list_tactical "first" Tacticals.New.tclFIRST +let () = register_list_tactical "solve" Tacticals.New.tclSOLVE + +let initial_tacticals () = + let idn n = Id.of_string (Printf.sprintf "_%i" n) in + let varn n = Reference (ArgVar (None, idn n)) in + let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in + List.iter iter [ + "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0]))); + "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0]))); + ] + +let () = Mltop.declare_cache_obj initial_tacticals "coretactics" diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index ed80dd7ae..d68139a4b 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -306,7 +306,7 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let p = EConstr.of_constr p in + let p = EConstr.of_constr @@ Universes.constr_of_global p in let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in @@ -735,7 +735,8 @@ let rewrite_except h = let refl_equal = let coq_base_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in function () -> (coq_base_constant "eq_refl") diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 51729f4c6..966b11d0e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -55,22 +55,16 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] -let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let lazy_find_reference dir s = + let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in + fun () -> Lazy.force gr -let try_find_global_reference dir s = - let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in - try Nametab.global_of_path sp - with Not_found -> - anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting") - -let find_reference dir s = - let gr = lazy (try_find_global_reference dir s) in - fun () -> Lazy.force gr +let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) let find_global dir s = - let gr = lazy (try_find_global_reference dir s) in + let gr = lazy (find_reference dir s) in fun (evd,cstrs) -> let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in @@ -81,7 +75,7 @@ let find_global dir s = (** Global constants. *) -let coq_eq_ref = find_reference ["Init"; "Logic"] "eq" +let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq" let coq_eq = find_global ["Init"; "Logic"] "eq" let coq_f_equal = find_global ["Init"; "Logic"] "f_equal" let coq_all = find_global ["Init"; "Logic"] "all" @@ -158,11 +152,11 @@ end) = struct let forall_relation = find_global morphisms "forall_relation" let pointwise_relation = find_global morphisms "pointwise_relation" - let forall_relation_ref = find_reference morphisms "forall_relation" - let pointwise_relation_ref = find_reference morphisms "pointwise_relation" + let forall_relation_ref = lazy_find_reference morphisms "forall_relation" + let pointwise_relation_ref = lazy_find_reference morphisms "pointwise_relation" let respectful = find_global morphisms "respectful" - let respectful_ref = find_reference morphisms "respectful" + let respectful_ref = lazy_find_reference morphisms "respectful" let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation" @@ -174,8 +168,8 @@ end) = struct let rewrite_relation_class = find_global relation_classes "RewriteRelation" - let proper_class = lazy (class_info (try_find_global_reference morphisms "Proper")) - let proper_proxy_class = lazy (class_info (try_find_global_reference morphisms "ProperProxy")) + let proper_class = lazy (class_info (find_reference morphisms "Proper")) + let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy")) let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs)))) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 053bb6fa1..7497aae3c 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -328,7 +328,6 @@ let selecti s m = module M = struct - open Coqlib open Constr open EConstr @@ -356,8 +355,8 @@ struct ["LRing_normalise"]] let coq_modules = - init_modules @ - [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules + Coqlib.(init_modules @ + [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules) let bin_module = [["Coq";"Numbers";"BinNums"]] @@ -375,8 +374,8 @@ struct * ZMicromega.v *) - let gen_constant_in_modules s m n = EConstr.of_constr (gen_constant_in_modules s m n) - let init_constant = gen_constant_in_modules "ZMicromega" init_modules + let gen_constant_in_modules s m n = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) + let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules let constant = gen_constant_in_modules "ZMicromega" coq_modules let bin_constant = gen_constant_in_modules "ZMicromega" bin_module let r_constant = gen_constant_in_modules "ZMicromega" r_modules @@ -1529,18 +1528,18 @@ let rec apply_ids t ids = | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids let coq_Node = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")) + lazy (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node") let coq_Leaf = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")) + lazy (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") let coq_Empty = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")) + lazy (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") let coq_VarMap = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")) + lazy (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t") let rec dump_varmap typ m = @@ -2059,8 +2058,8 @@ let micromega_order_changer cert env ff = [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); ("__varmap", vm, Term.mkApp - (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"), [|typ|])); + (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl))); diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index af8107025..6ba4c0f93 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -134,8 +134,10 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let tpexpr = - lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") +let gen_constant msg path s = Universes.constr_of_global @@ + coq_reference msg path s + +let tpexpr = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc") let ttvar = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEX") let ttadd = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEadd") @@ -541,7 +543,7 @@ let nsatz lpol = let return_term t = let a = - mkApp(gen_constant "CC" ["Init";"Logic"] "refl_equal",[|tllp ();t|]) in + mkApp(gen_constant "CC" ["Init";"Logic"] "eq_refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d3ca874bd..ee748567b 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -196,7 +196,7 @@ let coq_modules = init_modules @arith_modules @ [logic_dir] @ zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] -let gen_constant_in_modules n m s = EConstr.of_constr (gen_constant_in_modules n m s) +let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s) let init_constant = gen_constant_in_modules "Omega" init_modules let constant = gen_constant_in_modules "Omega" coq_modules diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index db69f1b40..7412de1e8 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -118,7 +118,8 @@ open Proofview.Notations the constants are loaded in the environment *) let constant dir s = - EConstr.of_constr (Coqlib.gen_constant "Quote" ("quote"::dir) s) + EConstr.of_constr @@ Universes.constr_of_global @@ + Coqlib.coq_reference "Quote" ("quote"::dir) s let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index a10ce68b4..fbed1df17 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -63,13 +63,13 @@ let coq_modules = let bin_module = [["Coq";"Numbers";"BinNums"]] let z_module = [["Coq";"ZArith";"BinInt"]] -let init_constant = Coqlib.gen_constant_in_modules "Omega" Coqlib.init_modules -let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules -let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module -let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module +let init_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x +let constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" coq_modules x +let z_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" z_module x +let bin_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" bin_module x (* Logic *) -let coq_refl_equal = lazy(init_constant "eq_refl") +let coq_refl_equal = lazy(init_constant "eq_refl") let coq_and = lazy(init_constant "and") let coq_not = lazy(init_constant "not") let coq_or = lazy(init_constant "or") @@ -133,7 +133,7 @@ let rec mk_nat = function let mkListConst c = let r = - Coqlib.gen_reference "" ["Init";"Datatypes"] c + Coqlib.coq_reference "" ["Init";"Datatypes"] c in let inst = if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|] diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index d580fde29..1b07a8ca8 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -22,28 +22,28 @@ let step_count = ref 0 let node_count = ref 0 -let logic_constant = - Coqlib.gen_constant "refl_tauto" ["Init";"Logic"] +let logic_constant s = Universes.constr_of_global @@ + Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s let li_False = lazy (destInd (logic_constant "False")) -let li_and = lazy (destInd (logic_constant "and")) -let li_or = lazy (destInd (logic_constant "or")) +let li_and = lazy (destInd (logic_constant "and")) +let li_or = lazy (destInd (logic_constant "or")) -let pos_constant = - Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"] +let pos_constant s = Universes.constr_of_global @@ + Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s let l_xI = lazy (pos_constant "xI") let l_xO = lazy (pos_constant "xO") let l_xH = lazy (pos_constant "xH") -let store_constant = - Coqlib.gen_constant "refl_tauto" ["rtauto";"Bintree"] +let store_constant s = Universes.constr_of_global @@ + Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s let l_empty = lazy (store_constant "empty") let l_push = lazy (store_constant "push") -let constant= - Coqlib.gen_constant "refl_tauto" ["rtauto";"Rtauto"] +let constant s = Universes.constr_of_global @@ + Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s let l_Reflect = lazy (constant "Reflect") diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 0e1225ada..38f05978d 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -230,7 +230,7 @@ let stdlib_modules = ] let coq_constant c = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)) + lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)) let coq_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) @@ -275,7 +275,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) @@ -284,7 +284,7 @@ let znew_ring_path = let zltac s = lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) -let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);; +let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);; let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; (* Ring theory *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e7b17991e..c2c8065a9 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -961,7 +961,6 @@ let expand_arg tms (p,ccl) ((_,t),_,na) = let k = length_of_tomatch_type_sign na t in (p+k,liftn_predicate (k-1) (p+1) ccl tms) - let use_unit_judge evd = let j, ctx = coq_unit_judge () in let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b944da750..bf62cea6b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -42,6 +42,31 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } +(*******************************************) +(* Functions to deal with impossible cases *) +(*******************************************) +(* XXX: we would like to search for this with late binding + "data.id.type" etc... *) +let impossible_default_case () = + let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in + let (_, u) = Term.destConst c in + Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx) + +let coq_unit_judge = + let open Environ in + let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in + let na1 = Name (Id.of_string "A") in + let na2 = Name (Id.of_string "H") in + fun () -> + match impossible_default_case () with + | Some (id, type_of_id, ctx) -> + make_judge id type_of_id, ctx + | None -> + (* In case the constants id/ID are not defined *) + Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) + (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), + Univ.ContextSet.empty + let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then @@ -351,7 +376,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = match ground_test with | Some result -> result | None -> - (* Until pattern-unification is used consistently, use nohdbeta to not + (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) let term1 = apprec_nohdbeta (fst ts) env evd term1 in let term2 = apprec_nohdbeta (fst ts) env evd term2 in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 7cee1e8a7..45857df2a 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -80,3 +80,5 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool -> Evarsolve.unification_result (**/**) +(** {6 Functions to deal with impossible cases } *) +val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set diff --git a/pretyping/program.ml b/pretyping/program.ml index de485dbe8..8769c5659 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -6,26 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open CErrors open Util -open Names -let make_dir l = DirPath.make (List.rev_map Id.of_string l) - -let find_reference locstr dir s = - let dp = make_dir dir in - let sp = Libnames.make_path dp (Id.of_string s) in - try Nametab.global_of_path sp - with Not_found -> - user_err (str "Library " ++ Libnames.pr_dirpath dp ++ - str " has to be required first.") - -let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s -let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) - -let init_constant dir s () = coq_constant "Program" dir s -let init_reference dir s () = coq_reference "Program" dir s +let init_constant dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s +let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = let open EConstr in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 768d6860d..fe44559ed 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -20,7 +20,7 @@ module NamedDecl = Context.Named.Declaration (* Absurd *) let mk_absurd_proof t = - let build_coq_not () = EConstr.of_constr (build_coq_not ()) in + let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in let id = Namegen.default_dependent_ident in mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]), mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|]))) @@ -35,7 +35,7 @@ let absurd c = let t = j.Environ.utj_val in let tac = Tacticals.New.tclTHENLIST [ - elim_type (EConstr.of_constr (build_coq_False ())); + elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ())); Simple.apply (mk_absurd_proof t) ] in Sigma.Unsafe.of_pair (tac, sigma) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 641929a77..bda25d7f0 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -106,8 +106,8 @@ let solveNoteqBranch side = let make_eq () = (*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) -let build_coq_not () = EConstr.of_constr (build_coq_not ()) -let build_coq_sumbool () = EConstr.of_constr (build_coq_sumbool ()) +let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) +let build_coq_sumbool () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_sumbool ()) let mkDecideEqGoal eqonleft op rectype c1 c2 = let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in diff --git a/tactics/equality.ml b/tactics/equality.ml index 839ec4ce1..e6278943d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -934,9 +934,9 @@ let build_selector env sigma dirn c ind special default = let ci = make_case_info env ind RegularStyle in mkCase (ci, p, c, Array.of_list brl) -let build_coq_False () = EConstr.of_constr (build_coq_False ()) -let build_coq_True () = EConstr.of_constr (build_coq_True ()) -let build_coq_I () = EConstr.of_constr (build_coq_I ()) +let build_coq_False () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()) +let build_coq_True () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_True ()) +let build_coq_I () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_I ()) let rec build_discriminator env sigma dirn c = function | [] -> @@ -1346,9 +1346,8 @@ let inject_if_homogenous_dependent_pair ty = pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in - let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" - ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in - let inj2 = EConstr.of_constr inj2 in + let inj2 = EConstr.of_constr @@ Universes.constr_of_global @@ + Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in (* cut with the good equality and prove the requested goal *) tclTHENLIST diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c7847e412..7e8cb4e63 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3521,12 +3521,11 @@ let error_ind_scheme s = let glob c = EConstr.of_constr (Universes.constr_of_global c) -let coq_eq = lazy (glob (Coqlib.build_coq_eq ())) +let coq_eq = lazy (glob (Coqlib.build_coq_eq ())) let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ())) -let coq_heq = lazy (EConstr.of_constr (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")) -let coq_heq_refl = lazy (EConstr.of_constr (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")) - +let coq_heq = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")) +let coq_heq_refl = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")) let mkEq t x y = mkApp (Lazy.force coq_eq, [| t; x; y |]) diff --git a/test-suite/Makefile b/test-suite/Makefile index c2d6e540c..b627f680b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -45,7 +45,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) # read out an emacs config and look for coq-prog-args; if such exists, return it get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1) -get_coq_prog_args = $(strip $(filter-out "-emacs-U" "-emacs",$(shell $(call get_coq_prog_args_helper,$(1))))) +get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) SINGLE_QUOTE=" #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter # wrap the arguments in parens, but only if they exist @@ -490,7 +490,7 @@ coq-makefile/%.log : coq-makefile/%/run.sh $(HIDE)(\ cd coq-makefile/$* && \ ./run.sh 2>&1; \ - if [ $$? = 0 ]; then \ + if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ else \ diff --git a/test-suite/coq-makefile/arg/run.sh b/test-suite/coq-makefile/arg/run.sh index 28b9bcb96..e98da17c7 100755 --- a/test-suite/coq-makefile/arg/run.sh +++ b/test-suite/coq-makefile/arg/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh index ccb348c6f..28d9878f9 100755 --- a/test-suite/coq-makefile/compat-subdirs/run.sh +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index e071f1db7..d6bb52bb4 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -11,10 +11,11 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . ./test +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index e071f1db7..d6bb52bb4 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -11,10 +11,11 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . ./test +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/extend-subdirs/run.sh b/test-suite/coq-makefile/extend-subdirs/run.sh index db1160113..ea5792a93 100755 --- a/test-suite/coq-makefile/extend-subdirs/run.sh +++ b/test-suite/coq-makefile/extend-subdirs/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/latex1/run.sh b/test-suite/coq-makefile/latex1/run.sh index 45f226911..214a9d5b2 100755 --- a/test-suite/coq-makefile/latex1/run.sh +++ b/test-suite/coq-makefile/latex1/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh index 9b89e5b6e..752c0c2ce 100755 --- a/test-suite/coq-makefile/merlin1/run.sh +++ b/test-suite/coq-makefile/merlin1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 418a2fb77..f6fb3bcb4 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -10,11 +10,12 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test ./test/test.glob +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 418a2fb77..f6fb3bcb4 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -10,11 +10,12 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test ./test/test.glob +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index a24a8a3cf..863c39f50 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -13,7 +13,7 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 097bd6398..bc9f846dd 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -12,11 +12,12 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test ./test/test.glob +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/only/run.sh b/test-suite/coq-makefile/only/run.sh index 4b471bcb8..2ea3deffb 100755 --- a/test-suite/coq-makefile/only/run.sh +++ b/test-suite/coq-makefile/only/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 684e0ece8..24ef8c891 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -11,7 +11,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index 684e0ece8..24ef8c891 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -11,7 +11,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index 684e0ece8..24ef8c891 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -11,7 +11,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index bfd2c1b95..bfd2c1b95 100644..100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index d24176279..e525e1208 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -13,7 +13,7 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh index d24176279..e525e1208 100755 --- a/test-suite/coq-makefile/uninstall2/run.sh +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -13,7 +13,7 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/validate1/run.sh b/test-suite/coq-makefile/validate1/run.sh index 61025021d..aaa4194b3 100755 --- a/test-suite/coq-makefile/validate1/run.sh +++ b/test-suite/coq-makefile/validate1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out new file mode 100644 index 000000000..bf1bf2809 --- /dev/null +++ b/test-suite/output/Show.out @@ -0,0 +1,12 @@ +3 subgoals (ID 29) + + H : 0 = 0 + ============================ + 1 = 1 + +subgoal 2 (ID 33) is: + 1 = S (S m') +subgoal 3 (ID 20) is: + S (S n') = S m + +(dependent evars: (printing disabled) ) diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v new file mode 100644 index 000000000..60faac8dd --- /dev/null +++ b/test-suite/output/Show.v @@ -0,0 +1,11 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) + +(* tests of Show output with -emacs flag to coqtop; see bug 5535 *) + +Theorem nums : forall (n m : nat), n = m -> (S n) = (S m). +Proof. + intros. + induction n as [| n']. + induction m as [| m']. + Show. +Admitted. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 5231899c6..fb064c495 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -184,7 +184,7 @@ CMOFILES = \ $(MLPACKFILES:.mlpack=.cmo) CMXFILES = $(CMOFILES:.cmo=.cmx) OFILES = $(CMXFILES:.cmx=.o) -CMAFILES = $(MLLIBFILES:.mllib=.cma) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) CMXAFILES = $(CMAFILES:.cma=.cmxa) CMIFILES = \ $(CMOFILES:.cmo=.cmi) \ @@ -474,6 +474,10 @@ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx $(SHOW)'CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 82d3d62b5..e06ef9d76 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -36,7 +36,7 @@ let is_keyword = "Hypothesis"; "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite"; "Implicit"; "Import"; "Inductive"; - "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; + "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Locate"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes"; @@ -58,9 +58,9 @@ let is_keyword = (*i (* coq terms *) *) "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; - "fix"; "cofix"; + "fix"; "cofix"; "is"; (* Ltac *) - "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; + "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; "type"; "of"; "rec"; (* Notations *) "level"; "associativity"; "no" ] @@ -70,7 +70,7 @@ let is_tactic = [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; - "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; + "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; "quote"; "eexact"; "autorewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 31d610abd..cf534f13a 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -62,9 +62,10 @@ let constr_of_global g = lazy (Universes.constr_of_global g) (* Some pre declaration of constant we are going to use *) let bb = constr_of_global Coqlib.glob_bool -let andb_prop = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb_prop +let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop let andb_true_intro = fun _ -> + Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_true_intro let tt = constr_of_global Coqlib.glob_true @@ -73,9 +74,9 @@ let ff = constr_of_global Coqlib.glob_false let eq = constr_of_global Coqlib.glob_eq -let sumbool = Coqlib.build_coq_sumbool +let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ()) -let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb +let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb let induct_on c = induction false None c None None @@ -849,7 +850,7 @@ let compute_dec_goal ind lnamesparrec nparrec = create_input ( mkNamedProd n (mkFullInd ind (2*nparrec)) ( mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( - mkApp(sumbool(),[|eqnm;mkApp (Coqlib.build_coq_not(),[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|]) ) ) ) diff --git a/vernac/command.ml b/vernac/command.ml index 4b29700e5..e2ebb4d7f 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -906,8 +906,9 @@ let subtac_dir = [contrib_name] let fixsub_module = subtac_dir @ ["Wf"] let tactics_module = subtac_dir @ ["Tactics"] -let init_reference dir s () = Coqlib.gen_reference "Command" dir s -let init_constant dir s () = EConstr.of_constr (Coqlib.gen_constant "Command" dir s) +let init_reference dir s () = Coqlib.coq_reference "Command" dir s +let init_constant dir s () = EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "Command" dir s) + let make_ref l s = init_reference l s let fix_proto = init_constant tactics_module "fix_proto" let fix_sub_ref = make_ref fixsub_module "Fix_sub" diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index a78221301..f57b1bba0 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -472,7 +472,8 @@ let build_combined_scheme env schemes = let ctx, ind, nargs = find_inductive t in (* Number of clauses, including the predicates quantification *) let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in - let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in + let coqand = Universes.constr_of_global @@ Coqlib.build_coq_and () in + let coqconj = Universes.constr_of_global @@ Coqlib.build_coq_conj () in let relargs = rel_vect 0 prods in let concls = List.rev_map (fun (cst, t) -> (* FIXME *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 64c156030..be58c67a9 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -260,7 +260,7 @@ let eterm_obligations env name evm fs ?status t ty = let tactics_module = ["Program";"Tactics"] let safe_init_constant md name () = Coqlib.check_required_library ("Coq"::md); - Coqlib.gen_constant "Obligations" md name + Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name) let hide_obligation = safe_init_constant tactics_module "obligation" let pperror cmd = CErrors.user_err ~hdr:"Program" cmd |