diff options
167 files changed, 847 insertions, 744 deletions
diff --git a/Makefile.dev b/Makefile.dev index 1803cc8ffe..fde92ec949 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 c48b830119..df75d5b93c 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/check.ml b/checker/check.ml index 11678fa6bb..6d93c11eac 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -72,7 +72,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (DirPath.to_string dir)) + user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir))) let library_full_filename dir = (find_library dir).library_filename diff --git a/checker/checker.ml b/checker/checker.ml index 5cadfe7b94..e00f47a540 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -335,7 +335,7 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); print_endline (Envars.coqlib ()); exit 0 @@ -373,7 +373,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); if_verbose print_header (); init_load_path (); engage (); diff --git a/checker/environ.ml b/checker/environ.ml index 7b59c6b986..bce40861cf 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -45,7 +45,7 @@ let set_engagement (impr_set as c) env = env.env_stratification.env_engagement in begin match impr_set,expected_impr_set with - | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement" + | PredicativeSet, ImpredicativeSet -> user_err Pp.(str "Incompatible engagement") | _ -> () end; { env with env_stratification = diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 27f79e7963..0482912b0a 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -535,13 +535,13 @@ let check_inductive env kn mib = (* check mind_finite : always OK *) (* check mind_ntypes *) if Array.length mib.mind_packets <> mib.mind_ntypes then - error "not the right number of packets"; + user_err Pp.(str "not the right number of packets"); (* check mind_params_ctxt *) let params = mib.mind_params_ctxt in let _ = check_ctxt env params in (* check mind_nparams *) if rel_context_nhyps params <> mib.mind_nparams then - error "number the right number of parameters"; + user_err Pp.(str "number the right number of parameters"); (* mind_packets *) (* - check arities *) let env_ar = typecheck_arity env params mib.mind_packets in diff --git a/checker/inductive.ml b/checker/inductive.ml index 8f23a38afc..9e417a8eb5 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -27,7 +27,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body let lookup_mind_specif env (kn,tyi) = let mib = lookup_mind kn env in if tyi >= Array.length mib.mind_packets then - error "Inductive.lookup_mind_specif: invalid inductive index"; + user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index"); (mib, mib.mind_packets.(tyi)) let find_rectype env c = @@ -232,7 +232,7 @@ let type_of_constructor_subst cstr u (mib,mip) = let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type."; + if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = diff --git a/checker/modops.ml b/checker/modops.ml index 07dda8a06d..bed31143bf 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -16,21 +16,21 @@ open Declarations (*i*) let error_not_a_constant l = - error ("\""^(Label.to_string l)^"\" is not a constant") + user_err Pp.(str ("\""^(Label.to_string l)^"\" is not a constant")) -let error_not_a_functor () = error "Application of not a functor" +let error_not_a_functor () = user_err Pp.(str "Application of not a functor") -let error_incompatible_modtypes _ _ = error "Incompatible module types" +let error_incompatible_modtypes _ _ = user_err Pp.(str "Incompatible module types") let error_not_match l _ = - error ("Signature components for label "^Label.to_string l^" do not match") + user_err Pp.(str ("Signature components for label "^Label.to_string l^" do not match")) -let error_no_such_label l = error ("No such label "^Label.to_string l) +let error_no_such_label l = user_err Pp.(str ("No such label "^Label.to_string l)) let error_no_such_label_sub l l1 = let l1 = ModPath.to_string l1 in - error ("The field "^ - Label.to_string l^" is missing in "^l1^".") + user_err Pp.(str ("The field "^ + Label.to_string l^" is missing in "^l1^".")) let error_not_a_module_loc ?loc s = user_err ?loc (str ("\""^Label.to_string s^"\" is not a module")) @@ -38,7 +38,7 @@ let error_not_a_module_loc ?loc s = let error_not_a_module s = error_not_a_module_loc s let error_with_module () = - error "Unsupported 'with' constraint in module implementation" + user_err Pp.(str "Unsupported 'with' constraint in module implementation") let is_functor = function | MoreFunctor _ -> true diff --git a/checker/reduction.ml b/checker/reduction.ml index 28c0126b41..82f09cf4b0 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -536,5 +536,5 @@ let dest_arity env c = let l, c = dest_prod_assum env c in match c with | Sort s -> l,s - | _ -> error "not an arity" + | _ -> user_err Pp.(str "not an arity") diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 53d80c6d55..c70cd5c8ce 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -40,7 +40,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - CErrors.error "Needs option -impredicative-set." + CErrors.user_err Pp.(str "Needs option -impredicative-set.") | _ -> () end; () @@ -61,7 +61,7 @@ let check_imports f caller env needed = let actual_stamp = lookup_digest env dp in if stamp <> actual_stamp then report_clash f caller dp with Not_found -> - error ("Reference to unknown module " ^ (DirPath.to_string dp)) + user_err Pp.(str ("Reference to unknown module " ^ (DirPath.to_string dp))) in Array.iter check needed diff --git a/checker/subtyping.ml b/checker/subtyping.ml index a290b240d8..2d04b77e46 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -302,22 +302,22 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err (Pp.str ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ - "name.")); + "name."))); if constant_has_body cb2 then error () ; let u = inductive_instance mind1 in let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err (Pp.str ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ - "name.")); + "name."))); if constant_has_body cb2 then error () ; let u1 = inductive_instance mind1 in let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in diff --git a/checker/term.ml b/checker/term.ml index 24e6008d34..8cac783753 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -273,14 +273,14 @@ let decompose_lam = abstractions *) let decompose_lam_n_assum n = if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match c with | Lambda (x,t,c) -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec empty_rel_context n @@ -306,14 +306,14 @@ let decompose_prod_assum = let decompose_prod_n_assum n = if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else match c with | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions") in prodec_rec empty_rel_context n diff --git a/checker/votour.ml b/checker/votour.ml index 48f9f45e7e..c255e5cdb2 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 1f7fbcbf68..bfa43cde1d 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 d52c184623..7fad65bf0a 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. @@ -162,7 +175,7 @@ uses type classes and rejects terms with unresolved holes. functions that used to carry a suffix `_loc`, such suffix has been dropped. -- `errorlabstrm` has been removed in favor of `user_err`. +- `errorlabstrm` and `error` has been removed in favor of `user_err`. - The header parameter to `user_err` has been made optional. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 0346c4a555..bb679ecba7 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/eConstr.ml b/engine/eConstr.ml index e5ac3792d6..c0485e4e76 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -295,7 +295,7 @@ let decompose_lam_assum sigma c = let decompose_lam_n_assum sigma n c = let open Rel.Declaration in if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -303,14 +303,14 @@ let decompose_lam_n_assum sigma n c = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec Context.Rel.empty n c let decompose_lam_n_decls sigma n = let open Rel.Declaration in if n < 0 then - error "decompose_lam_n_decls: integer parameter must be positive"; + user_err Pp.(str "decompose_lam_n_decls: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -318,7 +318,7 @@ let decompose_lam_n_decls sigma n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_decls: not enough abstractions" + | c -> user_err Pp.(str "decompose_lam_n_decls: not enough abstractions") in lamdec_rec Context.Rel.empty n @@ -363,7 +363,7 @@ let decompose_prod_assum sigma c = let decompose_prod_n_assum sigma n c = let open Rel.Declaration in if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else @@ -371,7 +371,7 @@ let decompose_prod_n_assum sigma n c = | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions") in prodec_rec Context.Rel.empty n c diff --git a/engine/evd.ml b/engine/evd.ml index 8ade6cb996..b677705bc9 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -952,7 +952,7 @@ let declare_principal_goal evk evd = | None -> { evd with future_goals = evk::evd.future_goals; principal_future_goal=Some evk; } - | Some _ -> CErrors.error "Only one main subgoal per instantiation." + | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.") let future_goals evd = evd.future_goals diff --git a/engine/proofview.ml b/engine/proofview.ml index 7f80d40d64..ddfc0e39dd 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -289,7 +289,7 @@ let tclONCE = Proof.once exception MoreThanOneSuccess let _ = CErrors.register_handler begin function - | MoreThanOneSuccess -> CErrors.error "This tactic has more than one success." + | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.") | _ -> raise CErrors.Unhandled end diff --git a/engine/termops.ml b/engine/termops.ml index 19e62f8e62..ca32c06a75 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 fe6dfb0ce1..58837ba033 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/engine/uState.ml b/engine/uState.ml index dc68220575..acef901432 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -188,7 +188,7 @@ let process_universe_constraints ctx cstrs = | _ -> local else begin match Univ.Universe.level r with - | None -> error ("Algebraic universe on the right") + | None -> user_err Pp.(str "Algebraic universe on the right") | Some r' -> if Univ.Level.is_small r' then let levels = Univ.Universe.levels l in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c7078cf2a0..4dcf287efc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -579,7 +579,7 @@ let rec subordinate_letins letins = function let terms_of_binders bl = let rec term_of_pat pt = CAst.map_with_loc (fun ?loc -> function | PatVar (Name id) -> CRef (Ident (loc,id), None) - | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term." + | PatVar (Anonymous) -> user_err Pp.(str "Cannot turn \"_\" into a term.") | PatCstr (c,l,_) -> let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in @@ -589,7 +589,7 @@ let terms_of_binders bl = | {loc; v = GLocalAssum (Name id,_,_)}::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l | {loc; v = GLocalDef (Name id,_,_,_)}::l -> extract_variables l | {loc; v = GLocalDef (Anonymous,_,_,_)}::l - | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> error "Cannot turn \"_\" into a term." + | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> user_err Pp.(str "Cannot turn \"_\" into a term.") | {loc; v = GLocalPattern ((u,_),_,_,_)}::l -> term_of_pat u :: extract_variables l | [] -> [] in extract_variables bl @@ -1862,7 +1862,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let eargs, rargs = extract_explicit_arg l args in if !parsing_explicit then if Id.Map.is_empty eargs then intern_args env subscopes rargs - else error "Arguments given by name or position not supported in explicit mode." + else user_err Pp.(str "Arguments given by name or position not supported in explicit mode.") else let rec aux n impl subscopes eargs rargs = let (enva,subscopes') = apply_scope_env env subscopes in diff --git a/interp/interp.mllib b/interp/interp.mllib index 607af82a03..6d290a325c 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/notation_ops.ml b/interp/notation_ops.ml index 74644b206a..6f91009111 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -42,7 +42,7 @@ let compare_glob_constr f add t1 t2 = match CAst.(t1.v,t2.v) with | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ | _,(GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) - -> error "Unsupported construction in recursive notations." + -> user_err Pp.(str "Unsupported construction in recursive notations.") | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ | GHole _ | GSort _ | GLetIn _), _ -> false @@ -112,7 +112,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with (* Re-interpret a notation as a glob_constr, taking care of binders *) let name_to_ident = function - | Anonymous -> CErrors.error "This expression should be a simple identifier." + | Anonymous -> CErrors.user_err Pp.(str "This expression should be a simple identifier.") | Name id -> id let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na @@ -377,7 +377,7 @@ let notation_constr_and_vars_of_glob_constr a = Array.iter (add_id found) idl; let dll = Array.map (List.map (fun (na,bk,oc,b) -> if bk != Explicit then - error "Binders marked as implicit not allowed in notations."; + user_err Pp.(str "Binders marked as implicit not allowed in notations."); add_name found na; (na,Option.map aux oc,aux b))) dll in NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k) @@ -387,7 +387,7 @@ let notation_constr_and_vars_of_glob_constr a = NHole (w, naming, arg) | GRef (r,_) -> NRef r | GEvar _ | GPatVar _ -> - error "Existential variables not allowed in notations." + user_err Pp.(str "Existential variables not allowed in notations.") ) x in let t = aux a in @@ -415,9 +415,9 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = Id.List.mem_assoc_sym x foundrec || Id.List.mem_assoc_sym x foundrecbinding then - error + user_err Pp.(str (Id.to_string x ^ - " should not be bound in a recursive pattern of the right-hand side.") + " should not be bound in a recursive pattern of the right-hand side.")) else injective := false in let check_pair s x y where = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1fe63c19c4..a79f10df6b 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -163,7 +163,7 @@ let split_at_annot bl na = match na with | None -> begin match names with - | [] -> error "A fixpoint needs at least one parameter." + | [] -> user_err (Pp.str "A fixpoint needs at least one parameter.") | _ -> ([], bl) end | Some (loc, id) -> diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index b1dd26119e..8515d51b0d 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1000,7 +1000,7 @@ let rec kl info m = if is_val m then (incr prune; term_of_fconstr m) else let (nm,s) = kni info m [] in - let _ = fapp_stack(nm,s) in (* to unlock Zupdates! *) + let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) zip_term (kl info) (norm_head info nm) s (* no redex: go up for atoms and already normalized terms, go down @@ -1050,7 +1050,7 @@ let inject c = mk_clos (subs_id 0) c let whd_stack infos m stk = let k = kni infos m stk in - let _ = fapp_stack k in (* to unlock Zupdates! *) + let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k (* cache of constants: the body is computed only when needed. *) diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 3f1cf92487..4533169804 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -71,7 +71,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = | _ -> Cpred.add c oracle.cst_trstate in { oracle with cst_opacity; cst_trstate; } - | RelKey _ -> CErrors.error "set_strategy: RelKey" + | RelKey _ -> CErrors.user_err Pp.(str "set_strategy: RelKey") let fold_strategy f { var_opacity; cst_opacity; } accu = let fvar id lvl accu = f (VarKey id) lvl accu in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d8d365c347..4f4b641b44 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -25,7 +25,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body let lookup_mind_specif env (kn,tyi) = let mib = Environ.lookup_mind kn env in if tyi >= Array.length mib.mind_packets then - error "Inductive.lookup_mind_specif: invalid inductive index"; + user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index"); (mib, mib.mind_packets.(tyi)) let find_rectype env c = @@ -247,7 +247,7 @@ let type_of_constructor (cstr, u) (mib,mip) = let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type."; + if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = diff --git a/kernel/names.ml b/kernel/names.ml index f5b3f4e007..afdbe0c0dc 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -35,7 +35,7 @@ struct let hash = String.hash let check_valid ?(strict=true) x = - let iter (fatal, x) = if fatal || strict then CErrors.error x in + let iter (fatal, x) = if fatal || strict then CErrors.user_err Pp.(str x) in Option.iter iter (Unicode.ident_refutation x) let is_valid s = match Unicode.ident_refutation s with diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 6bd82170e6..26d0617683 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -125,7 +125,7 @@ let call_linker ?(fatal=true) prefix f upds = if not (Sys.file_exists f) then begin let msg = "Cannot find native compiler file " ^ f in - if fatal then CErrors.error msg + if fatal then CErrors.user_err Pp.(str msg) else if !Flags.debug then Feedback.msg_debug (Pp.str msg) end else diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index d0593c0e05..502a10113d 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -36,12 +36,11 @@ let empty_opaquetab = { (* hooks *) let default_get_opaque dp _ = - CErrors.error - ("Cannot access opaque proofs in library " ^ DirPath.to_string dp) + CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp]) let default_get_univ dp _ = - CErrors.error - ("Cannot access universe constraints of opaque proofs in library " ^ - DirPath.to_string dp) + CErrors.user_err (Pp.pr_sequence Pp.str [ + "Cannot access universe constraints of opaque proofs in library "; + DirPath.to_string dp]) let get_opaque = ref default_get_opaque let get_univ = ref default_get_univ diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index caaaff1b89..f5e8e86530 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -192,7 +192,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - CErrors.error "Needs option -impredicative-set." + CErrors.user_err Pp.(str "Needs option -impredicative-set.") | _ -> () end @@ -346,10 +346,10 @@ let check_required current_libs needed = try let actual = DPMap.find id current_libs in if not(digest_match ~actual ~required) then - CErrors.error - ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") + CErrors.user_err Pp.(pr_sequence str + ["Inconsistent assumptions over module"; DirPath.to_string id; "."]) with Not_found -> - CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".") + CErrors.user_err Pp.(pr_sequence str ["Reference to unknown module"; DirPath.to_string id; "."]) in Array.iter check needed @@ -367,7 +367,7 @@ let safe_push_named d env = let _ = try let _ = Environ.lookup_named id env in - CErrors.error ("Identifier "^Id.to_string id^" already defined.") + CErrors.user_err Pp.(pr_sequence str ["Identifier"; Id.to_string id; "already defined."]) with Not_found -> () in Environ.push_named d env @@ -908,7 +908,7 @@ let register_inline kn senv = let open Environ in let open Pre_env in if not (evaluable_constant kn senv.env) then - CErrors.error "Register inline: an evaluable constant is expected"; + CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); let env = pre_env senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index d0fdf9fdae..f779f68be4 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -110,8 +110,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 in let u = if poly then - CErrors.error ("Checking of subtyping of polymorphic" ^ - " inductive types not implemented") + CErrors.user_err Pp.(str "Checking of subtyping of polymorphic inductive types not implemented") else Instance.empty in let mib2 = Declareops.subst_mind_body subst2 mib2 in @@ -347,7 +346,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = Mod_subst.force_constr lc2 in check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -364,7 +363,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error = NotConvertibleTypeField (env, arity1, typ2) in check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/kernel/term.ml b/kernel/term.ml index 03562d9f31..a4296a530c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -526,26 +526,26 @@ let decompose_lam = (* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T) *) let decompose_prod_n n = - if n < 0 then error "decompose_prod_n: integer parameter must be positive"; + if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | _ -> error "decompose_prod_n: not enough products" + | _ -> user_err (str "decompose_prod_n: not enough products") in prodec_rec [] n (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T) *) let decompose_lam_n n = - if n < 0 then error "decompose_lam_n: integer parameter must be positive"; + if n < 0 then user_err (str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | _ -> error "decompose_lam_n: not enough abstractions" + | _ -> user_err (str "decompose_lam_n: not enough abstractions") in lamdec_rec [] n @@ -581,7 +581,7 @@ let decompose_lam_assum = ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *) let decompose_prod_n_assum n = if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; + user_err (str "decompose_prod_n_assum: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else @@ -590,7 +590,7 @@ let decompose_prod_n_assum n = | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + | c -> user_err (str "decompose_prod_n_assum: not enough assumptions") in prodec_rec Context.Rel.empty n @@ -602,7 +602,7 @@ let decompose_prod_n_assum n = but n is the actual number of destructurated lambdas. *) let decompose_lam_n_assum n = if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; + user_err (str "decompose_lam_n_assum: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -611,14 +611,14 @@ let decompose_lam_n_assum n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + | c -> user_err (str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec Context.Rel.empty n (* Same, counting let-in *) let decompose_lam_n_decls n = if n < 0 then - error "decompose_lam_n_decls: integer parameter must be positive"; + user_err (str "decompose_lam_n_decls: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -627,7 +627,7 @@ let decompose_lam_n_decls n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_decls: not enough abstractions" + | c -> user_err (str "decompose_lam_n_decls: not enough abstractions") in lamdec_rec Context.Rel.empty n diff --git a/lib/cErrors.ml b/lib/cErrors.ml index b55fd80c68..b0e77a4c90 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -38,7 +38,6 @@ exception UserError of string option * std_ppcmds (* User errors *) let todo s = prerr_string ("TODO: "^s^"\n") let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) -let error string = user_err (str string) let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) @@ -138,3 +137,8 @@ let handled e = let bottom _ = raise Bottom in try let _ = print_gen bottom !handle_stack e in true with Bottom -> false + +(* Deprecated functions *) +let error string = user_err (str string) +let user_err_loc (loc,hdr,msg) = user_err ~loc ~hdr msg +let errorlabstrm hdr msg = user_err ~hdr msg diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 0665a8ce73..ca0838575e 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -41,9 +41,6 @@ val user_err : ?loc:Loc.t -> ?hdr:string -> std_ppcmds -> 'a (** Main error raising primitive. [user_err ?loc ?hdr pp] signals an error [pp] with optional header and location [hdr] [loc] *) -val error : string -> 'a -(** [error s] just calls [user_error "_" (str s)] *) - exception AlreadyDeclared of std_ppcmds val alreadydeclared : std_ppcmds -> 'a @@ -98,3 +95,14 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool + +(** Deprecated functions *) +val error : string -> 'a + [@@ocaml.deprecated "use [user_err] instead"] + +val errorlabstrm : string -> std_ppcmds -> 'a + [@@ocaml.deprecated "use [user_err ~hdr] instead"] + +val user_err_loc : Loc.t * string * std_ppcmds -> 'a + [@@ocaml.deprecated "use [user_err ~loc] instead"] + diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 2755946abc..d004fd6711 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -86,7 +86,7 @@ let parse_flag s = | '+' -> (AsError, String.sub s 1 (String.length s - 1)) | '-' -> (Disabled, String.sub s 1 (String.length s - 1)) | _ -> (Enabled, s) - else CErrors.error "Invalid warnings flag" + else CErrors.user_err Pp.(str "Invalid warnings flag") let string_of_flag (status,name) = match status with diff --git a/interp/coqlib.ml b/library/coqlib.ml index 9539980f04..955ff4c089 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 1facb47e1e..716d97c9d0 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/declaremods.ml b/library/declaremods.ml index 3a263b1e12..08c33b5c15 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -345,7 +345,7 @@ let get_applications mexpr = let rec get params = function | MEident mp -> mp, params | MEapply (fexpr, mp) -> get (mp::params) fexpr - | MEwith _ -> error "Non-atomic functor application." + | MEwith _ -> user_err Pp.(str "Non-atomic functor application.") in get [] mexpr (** Create the substitution corresponding to some functor applications *) @@ -353,7 +353,7 @@ let get_applications mexpr = let rec compute_subst env mbids sign mp_l inl = match mbids,mp_l with | _,[] -> mbids,empty_subst - | [],r -> error "Application of a functor with too few arguments." + | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") | mbid::mbids,mp::mp_l -> let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mb = Environ.lookup_module mp env in @@ -777,7 +777,7 @@ let rec decompose_functor mpl typ = match mpl, typ with | [], _ -> typ | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str - | _ -> error "Application of a functor with too much arguments." + | _ -> user_err Pp.(str "Application of a functor with too much arguments.") exception NoIncludeSelf diff --git a/library/goptions.ml b/library/goptions.ml index 9b4fc99857..a803771cbc 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -71,7 +71,7 @@ module MakeTable = let _ = if String.List.mem_assoc nick !A.table then - error "Sorry, this table name is already used." + user_err Pp.(str "Sorry, this table name is already used.") module MySet = Set.Make (struct type t = A.t let compare = A.compare end) @@ -214,11 +214,11 @@ let get_option key = OptionMap.find key !value_tab let check_key key = try let _ = get_option key in - error "Sorry, this option name is already used." + user_err Pp.(str "Sorry, this option name is already used.") with Not_found -> if String.List.mem_assoc (nickname key) !string_table || String.List.mem_assoc (nickname key) !ref_table - then error "Sorry, this option name is already used." + then user_err Pp.(str "Sorry, this option name is already used.") open Libobject @@ -307,7 +307,7 @@ let set_option_value locality check_and_cast key v = | Some (name, depr, (read,write,append)) -> write (get_locality locality) (check_and_cast v (read ())) -let bad_type_error () = error "Bad type of value for this option." +let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") let check_int_value v = function | IntValue _ -> IntValue v diff --git a/library/impargs.ml b/library/impargs.ml index a63264b669..885185da1a 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -364,7 +364,7 @@ let set_manual_implicits env flags enriching autoimps l = with Not_found -> l, None in if not (List.distinct l) then - error ("Some parameters are referred more than once."); + user_err Pp.(str "Some parameters are referred more than once."); (* Compare with automatic implicits to recover printing data and names *) let rec merge k l = function | (Name id,imp)::imps -> @@ -658,7 +658,7 @@ let check_inclusion l = let rec aux = function | n1::(n2::_ as nl) -> if n1 <= n2 then - error "Sequences of implicit arguments must be of different lengths."; + user_err Pp.(str "Sequences of implicit arguments must be of different lengths."); aux nl | _ -> () in aux (List.map (fun (imps,_) -> List.length imps) l) diff --git a/library/lib.ml b/library/lib.ml index ddd2ed6afa..4ad4e261d7 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -76,7 +76,7 @@ let classify_segment seg = (* LEM; TODO: Understand what this does and see if what I do is the correct thing for ClosedMod(ule|type) *) | (_,ClosedModule _) :: stk -> clean acc stk - | (_,OpenedSection _) :: _ -> error "there are still opened sections" + | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections") | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" (str "there are still opened " ++ str (module_kind ty) ++ str "s") @@ -184,7 +184,7 @@ let split_lib_gen test = | [] -> None in match findeq [] !lib_state.lib_stk with - | None -> error "no such entry" + | None -> user_err Pp.(str "no such entry") | Some r -> r let eq_object_name (fp1, kn1) (fp2, kn2) = @@ -222,7 +222,7 @@ let add_anonymous_entry node = let add_leaf id obj = if Names.ModPath.equal (current_mp ()) Names.initial_path then - error ("No session module started (use -top dir)"); + user_err Pp.(str "No session module started (use -top dir)"); let oname = make_oname id in cache_object (oname,obj); add_entry oname (Leaf obj); @@ -272,8 +272,8 @@ let current_mod_id () = try match find_entry_p is_opening_node_or_lib with | oname,OpenedModule (_,_,_,fs) -> basename (fst oname) | oname,CompilingLibrary _ -> basename (fst oname) - | _ -> error "you are not in a module" - with Not_found -> error "no opened modules" + | _ -> user_err Pp.(str "you are not in a module") + with Not_found -> user_err Pp.(str "no opened modules") let start_mod is_type export id mp fs = @@ -305,7 +305,7 @@ let end_mod is_type = else error_still_opened (module_kind ty) oname | oname,OpenedSection _ -> error_still_opened "section" oname | _ -> assert false - with Not_found -> error "No opened modules." + with Not_found -> user_err (Pp.str "No opened modules.") in let (after,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; @@ -326,9 +326,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after (* TODO: use check_for_module ? *) let start_compilation s mp = if !lib_state.comp_name != None then - error "compilation unit is already started"; + user_err Pp.(str "compilation unit is already started"); if not (Names.DirPath.is_empty (current_sections ())) then - error "some sections are already opened"; + user_err Pp.(str "some sections are already opened"); let prefix = s, (mp, Names.DirPath.empty) in let () = add_anonymous_entry (CompilingLibrary prefix) in lib_state := { !lib_state with comp_name = Some s; @@ -337,7 +337,7 @@ let start_compilation s mp = let end_compilation_checks dir = let _ = try match snd (find_entry_p is_opening_node) with - | OpenedSection _ -> error "There are some open sections." + | OpenedSection _ -> user_err Pp.(str "There are some open sections.") | OpenedModule (ty,_,_,_) -> user_err ~hdr:"Lib.end_compilation_checks" (str "There are some open " ++ str (module_kind ty) ++ str "s.") @@ -394,7 +394,7 @@ let find_opening_node id = user_err ~hdr:"Lib.find_opening_node" (str "Last block to end has name " ++ pr_id id' ++ str "."); entry - with Not_found -> error "There is nothing to end." + with Not_found -> user_err Pp.(str "There is nothing to end.") (* Discharge tables *) @@ -428,7 +428,7 @@ let add_section () = let check_same_poly p vars = let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in if List.exists pred vars then - error "Cannot mix universe polymorphic and monomorphic declarations in sections." + user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") let add_section_variable id impl poly ctx = match !sectab with @@ -555,7 +555,7 @@ let close_section () = | oname,OpenedSection (_,fs) -> oname,fs | _ -> assert false with Not_found -> - error "No opened section." + user_err Pp.(str "No opened section.") in let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; diff --git a/library/libnames.ml b/library/libnames.ml index dd74e192ff..50f28b0205 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -58,14 +58,14 @@ let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p) let parse_dir s = let len = String.length s in let rec decoupe_dirs dirs n = - if Int.equal n len && n > 0 then error (s ^ " is an invalid path."); + if Int.equal n len && n > 0 then user_err Pp.(str @@ s ^ " is an invalid path."); if n >= len then dirs else let pos = try String.index_from s n '.' with Not_found -> len in - if Int.equal pos n then error (s ^ " is an invalid path."); + if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path."); let dir = String.sub s n (pos-n) in decoupe_dirs ((Id.of_string dir)::dirs) (pos+1) in diff --git a/library/library.ml b/library/library.ml index 2b3381fa7c..5a5f99cc51 100644 --- a/library/library.ml +++ b/library/library.ml @@ -764,7 +764,7 @@ let save_library_to ?todo dir f otab = if !Flags.native_compiler then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Nativelib.compile_library dir ast fn) then - error "Could not compile the library to native code." + user_err Pp.(str "Could not compile the library to native code.") with reraise -> let reraise = CErrors.push reraise in let () = Feedback.msg_warning (str "Removed file " ++ str f') in diff --git a/library/library.mllib b/library/library.mllib index df4f735034..6f433b77d1 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -16,3 +16,4 @@ Goptions Decls Heads Keys +Coqlib diff --git a/library/nametab.ml b/library/nametab.ml index 1027e291ce..2e4e98013e 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -143,8 +143,8 @@ struct (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) (* But ours is also absolute! This is an error! *) - error ("Cannot mask the absolute name \"" - ^ U.to_string uname' ^ "\"!") + user_err Pp.(str @@ "Cannot mask the absolute name \"" + ^ U.to_string uname' ^ "\"!") | Nothing | Relative _ -> mktree (Absolute (uname,o)) tree.map diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b5d0780bd5..893605499c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -660,7 +660,7 @@ GEXTEND Gram if Option.is_empty !slash_position then (slash_position := Some i; parse_args i args) else - error "The \"/\" modifier can occur only once" + user_err Pp.(str "The \"/\" modifier can occur only once") in let args = parse_args 0 (List.flatten args) in let more_implicits = Option.default [] more_implicits in @@ -734,7 +734,7 @@ GEXTEND Gram | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x - | Some _, Some _ -> error "scope declared twice" in + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; @@ -742,7 +742,7 @@ GEXTEND Gram | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x - | Some _, Some _ -> error "scope declared twice" in + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; @@ -750,7 +750,7 @@ GEXTEND Gram | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x - | Some _, Some _ -> error "scope declared twice" in + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; @@ -939,7 +939,7 @@ GEXTEND Gram PrintGrammar ent | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir | IDENT "Modules" -> - error "Print Modules is obsolete; use Print Libraries instead" + user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") | IDENT "Libraries" -> PrintModules | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index a0b04ce3b5..33a9dd4fd9 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 201726d1e6..b3017f359b 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/derive/derive.ml b/plugins/derive/derive.ml index 12d7f06603..b3ab29cced 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -53,9 +53,9 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted _ -> CErrors.error"Admitted isn't supported in Derive." + | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") | Proved (_,Some _,_) -> - CErrors.error"Cannot save a proof of Derive with an explicit name." + CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 322fbcea74..2c85b185c4 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -41,7 +41,7 @@ let toplevel_env () = | "MODULE TYPE" -> let modtype = Global.lookup_modtype (MPdot (mp, l)) in Some (l, SFBmodtype modtype) - | "INCLUDE" -> error "No extraction of toplevel Include yet." + | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.") | _ -> None end | _ -> None @@ -435,7 +435,7 @@ let mono_filename f = else try Id.of_string (Filename.basename f) with UserError _ -> - error "Extraction: provided filename is not a valid identifier" + user_err Pp.(str "Extraction: provided filename is not a valid identifier") in Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 0692c88cd1..b580fb5925 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -185,7 +185,7 @@ let rec pp_expr par env args = pp_boxed_tuple (pp_expr true env []) l | MLcase (_,t, pv) when is_custom_match pv -> if not (is_regular_match pv) then - error "Cannot mix yet user-given match and general patterns."; + user_err Pp.(str "Cannot mix yet user-given match and general patterns."); let mkfun (ids,_,e) = if not (List.is_empty ids) then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index d8e3821557..4399fc561f 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -246,7 +246,7 @@ let rec pp_expr par env args = pp_boxed_tuple (pp_expr true env []) l | MLcase (_, t, pv) when is_custom_match pv -> if not (is_regular_match pv) then - error "Cannot mix yet user-given match and general patterns."; + user_err Pp.(str "Cannot mix yet user-given match and general patterns."); let mkfun (ids,_,e) = if not (List.is_empty ids) then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 8d0cc4a0db..3c81564e34 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -96,9 +96,9 @@ let rec pp_expr env args = prlist_with_sep spc (pp_cons_args env) args') in if is_coinductive r then paren (str "delay " ++ st) else st - | MLtuple _ -> error "Cannot handle tuples in Scheme yet." + | MLtuple _ -> user_err Pp.(str "Cannot handle tuples in Scheme yet.") | MLcase (_,_,pv) when not (is_regular_match pv) -> - error "Cannot handle general patterns in Scheme yet." + user_err Pp.(str "Cannot handle general patterns in Scheme yet.") | MLcase (_,t,pv) when is_custom_match pv -> let mkfun (ids,_,e) = if not (List.is_empty ids) then named_lams (List.rev ids) e diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 5a1e7c26a1..4c6355f61c 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -161,7 +161,7 @@ let left_instance_tac (inst,id) continue seq= let evmap, _ = try Typing.type_of (pf_env gl) evmap gt with e when CErrors.noncritical e -> - error "Untypable instance, maybe higher-order non-prenex quantification" in + user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in Sigma.Unsafe.of_pair (generalize [gt], evmap) end }) else diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 86a6770070..8c6b5b91de 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/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 2d18b66054..826afc35b6 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -227,7 +227,7 @@ let extend_with_auto_hints env sigma l seq = try searchtable_map dbname with Not_found-> - error ("Firstorder: "^dbname^" : No such Hint database") in + user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in Hint_db.iter g hdb in List.iter h l; !seqref, sigma (*FIXME: forgetting about universes*) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 25d8f8c832..a6290cb00c 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"] @@ -513,11 +514,11 @@ let rec fourier () = with NoIneq -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then CErrors.error "No inequalities"; + if !lineq=[] then CErrors.user_err Pp.(str "No inequalities"); let res=fourier_lineq (!lineq) in let tac=ref (Proofview.tclUNIT ()) in if res=[] - then CErrors.error "fourier failed" + then CErrors.user_err Pp.(str "fourier failed") (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 55d361e3d2..434fb14a6e 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 @@ -820,10 +820,10 @@ let build_proof build_proof new_finalize {dyn_infos with info = f } g end | Fix _ | CoFix _ -> - error ( "Anonymous local (co)fixpoints are not handled yet") + user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) - | Proj _ -> error "Prod" - | Prod _ -> error "Prod" + | Proj _ -> user_err Pp.(str "Prod") + | Prod _ -> user_err Pp.(str "Prod") | LetIn _ -> let new_infos = { dyn_infos with @@ -1097,7 +1097,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (Global.env ()) (Evd.empty) (EConstr.of_constr body) - | None -> error ( "Cannot define a principle over an axiom ") + | None -> user_err Pp.(str "Cannot define a principle over an axiom ") in let fbody = get_body fnames.(fun_num) in let f_ctxt,f_body = decompose_lam (project g) fbody in @@ -1199,7 +1199,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam bs.(num), List.rev_map var_of_decl princ_params)) ),num - | _ -> error "Not a mutual block" + | _ -> user_err Pp.(str "Not a mutual block") in let info = {infos with @@ -1594,9 +1594,9 @@ let prove_principle_for_gen let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in let lemma = match !tcc_lemma_ref with - | Undefined -> error "No tcc proof !!" + | 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/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 529b91c4ca..18d63dd94b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -75,7 +75,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let rel_as_kn = fst (match princ_type_info.indref with | Some (Globnames.IndRef ind) -> ind - | _ -> error "Not a valid predicate" + | _ -> user_err Pp.(str "Not a valid predicate") ) in let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in @@ -416,7 +416,7 @@ let get_funs_constant mp dp = in let body = EConstr.Unsafe.to_constr body in body - | None -> error ( "Cannot define a principle over an axiom ") + | None -> user_err Pp.(str ( "Cannot define a principle over an axiom ")) in let f = find_constant_body const in let l_const = get_funs_constant const f in @@ -432,7 +432,7 @@ let get_funs_constant mp dp = List.iter (fun params -> if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params) - then error "Not a mutal recursive block" + then user_err Pp.(str "Not a mutal recursive block") ) l_params in @@ -445,7 +445,7 @@ let get_funs_constant mp dp = | _ -> if is_first && Int.equal (List.length l_bodies) 1 then raise Not_Rec - else error "Not a mutal recursive block" + else user_err Pp.(str "Not a mutal recursive block") in let first_infos = extract_info true (List.hd l_bodies) in let check body = (* Hope this is correct *) @@ -454,7 +454,7 @@ let get_funs_constant mp dp = Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2 in if not (eq_infos first_infos (extract_info false body)) - then error "Not a mutal recursive block" + then user_err Pp.(str "Not a mutal recursive block") in List.iter check l_bodies with Not_Rec -> () diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 5e6128b1b9..1db8be0818 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -90,7 +90,7 @@ let pr_intro_as_pat _prc _ _ pat = let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) - | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected." + | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.") ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] @@ -228,7 +228,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> - CErrors.error ("Cannot generate induction principle(s)") + CErrors.user_err Pp.(str "Cannot generate induction principle(s)") | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7f2b21e79d..68e097fe9c 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 @@ -576,8 +576,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = WARNING: We need to restart since [b] itself should be an application term *) build_entry_lc env funnames avoid (mkGApp(b,args)) - | GRec _ -> error "Not handled GRec" - | GProd _ -> error "Cannot apply a type" + | GRec _ -> user_err Pp.(str "Not handled GRec") + | GProd _ -> user_err Pp.(str "Cannot apply a type") end (* end of the application treatement *) | GLambda(n,_,t,b) -> @@ -678,7 +678,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc env funnames avoid match_expr end - | GRec _ -> error "Not handled GRec" + | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,_) -> build_entry_lc env funnames avoid b and build_entry_lc_from_case env funname make_discr diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 5abcb100f7..0361e8cb13 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - CAst.map (function + CAst.map_with_loc (fun ?loc -> function | GRef _ as x -> x | GVar id -> let new_id = @@ -172,7 +172,7 @@ let change_vars = change_vars mapping lhs, change_vars mapping rhs ) - | GRec _ -> error "Local (co)fixes are not supported" + | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported") | GSort _ as x -> x | GHole _ as x -> x | GCast(b,c) -> @@ -352,7 +352,7 @@ let rec alpha_rt excluded rt = alpha_rt excluded lhs, alpha_rt excluded rhs ) - | GRec _ -> error "Not handled GRec" + | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ | GHole _ as rt -> rt | GCast (b,c) -> @@ -408,7 +408,7 @@ let is_free_in id = | GIf(cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | GRec _ -> raise (UserError(None,str "Not handled GRec")) + | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t @@ -695,7 +695,7 @@ let expand_as = | GIf(e,(na,po),br1,br2) -> GIf(expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) - | GRec _ -> error "Not handled GRec" + | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,c) -> GCast(expand_as map b, Miscops.map_cast_type (expand_as map) c) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index ab83cb15a6..74c0eb4cc7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -186,6 +186,8 @@ let build_newrecursive l = in build_newrecursive l' +let error msg = user_err Pp.(str msg) + (* Checks whether or not the mutual bloc is recursive *) let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index ea985ddecd..2476478abe 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 ()) *) @@ -502,13 +510,13 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; let decompose_lam_n sigma n = - if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive"; + if n < 0 then CErrors.user_err Pp.(str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match EConstr.kind sigma c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | _ -> CErrors.error "decompose_lam_n: not enough abstractions" + | _ -> CErrors.user_err Pp.(str "decompose_lam_n: not enough abstractions") in lamdec_rec [] n diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8c972cd7cf..d68bdc2153 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -197,7 +197,7 @@ let generate_type evd g_to_f f graph i = let find_induction_principle evd f = let f_as_constant,u = match EConstr.kind !evd f with | Const c' -> c' - | _ -> error "Must be used with a function" + | _ -> user_err Pp.(str "Must be used with a function") in let infos = find_Function_infos f_as_constant in match infos.rect_lemma with @@ -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[ @@ -701,7 +701,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let graph_def = graphs.(j) in let infos = try find_Function_infos (fst (destConst (project g) funcs.(j))) - with Not_found -> error "No graph found" + with Not_found -> user_err Pp.(str "No graph found") in if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs @@ -1006,6 +1006,7 @@ let functional_inversion kn hid fconst f_correct : tactic = | _ -> tclFAIL 1 (mt ()) g +let error msg = user_err Pp.(str msg) let invfun qhyp f = let f = diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b99a05dfbc..b2c8489ce1 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -347,7 +347,7 @@ let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list = filter_shift_stable lnk (Array.to_list larr) - +let error msg = user_err Pp.(str msg) (** {1 Utilities for merging} *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c463093553..2f9f708768 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 @@ -136,7 +138,7 @@ let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" - with Not_found -> error "module Recdef not loaded" + with Not_found -> user_err Pp.(str "module Recdef not loaded") let iter = function () -> (constr_of_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") @@ -323,8 +325,8 @@ let check_not_nested sigma forbidden e = | Construct _ -> () | Case(_,t,e,a) -> check_not_nested t;check_not_nested e;Array.iter check_not_nested a - | Fix _ -> error "check_not_nested : Fix" - | CoFix _ -> error "check_not_nested : Fix" + | Fix _ -> user_err Pp.(str "check_not_nested : Fix") + | CoFix _ -> user_err Pp.(str "check_not_nested : Fix") in try check_not_nested e @@ -430,8 +432,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = let sigma = project g in match EConstr.kind sigma expr_info.info with - | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint" - | Proj _ -> error "Function cannot treat projections" + | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") + | Proj _ -> user_err Pp.(str "Function cannot treat projections") | LetIn(na,b,t,e) -> begin let new_continuation_tac = @@ -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 @@ -1304,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp in let na = next_global_ident_away name [] in if Termops.occur_existential sigma gls_type then - CErrors.error "\"abstract\" cannot handle existentials"; + CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = let na_ref = Libnames.Ident (Loc.tag na) in diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 6890b31981..0a13a20a97 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/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 470a93f2bc..bf84f61a5b 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -56,17 +56,16 @@ let instantiate_tac n c ido = InHyp -> (match decl with | LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ) - | _ -> error - "Please be more specific: in type or value?") + | _ -> user_err Pp.(str "Please be more specific: in type or value?")) | InHypTypeOnly -> evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl)) | InHypValueOnly -> (match decl with | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body) - | _ -> error "Not a defined hypothesis.") in + | _ -> user_err Pp.(str "Not a defined hypothesis.")) in if List.length evl < n then - error "Not enough uninstantiated existential variables."; - if n <= 0 then error "Incorrect existential variable index."; + user_err Pp.(str "Not enough uninstantiated existential variables."); + if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let evk,_ = List.nth evl (n-1) in instantiate_evar evk c sigma gl end @@ -76,7 +75,7 @@ let instantiate_tac_by_name id c = let sigma = gl.sigma in let evk = try Evd.evar_key id sigma - with Not_found -> error "Unknown existential variable." in + with Not_found -> user_err Pp.(str "Unknown existential variable.") in instantiate_evar evk c sigma gl end @@ -109,8 +108,8 @@ let hget_evar n = let concl = Proofview.Goal.concl gl in let evl = evar_list sigma concl in if List.length evl < n then - error "Not enough uninstantiated existential variables."; - if n <= 0 then error "Incorrect existential variable index."; + user_err Pp.(str "Not enough uninstantiated existential variables."); + if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let ev = List.nth evl (n-1) in let ev_type = EConstr.existential_type sigma ev in Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index a3310c2d8c..fdb8d34618 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -90,7 +90,7 @@ let occurrences_of = function | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) | nl -> if List.exists (fun n -> n < 0) nl then - CErrors.error "Illegal negative occurrence number."; + CErrors.user_err Pp.(str "Illegal negative occurrence number."); OnlyOccurrences nl let coerce_to_int v = match Value.to_int v with diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index cbd8a7f0fe..d68139a4b4 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") @@ -1084,7 +1085,7 @@ let decompose l c = let sigma = Tacmach.New.project gl in let to_ind c = if isInd sigma c then fst (destInd sigma c) - else error "not an inductive type" + else user_err Pp.(str "not an inductive type") in let l = List.map to_ind l in Elim.h_decompose l c diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 257100b012..1404b1c1f1 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -117,8 +117,8 @@ let mk_fix_tac (loc,id,bl,ann,ty) = | _, Some x -> let ids = List.map snd (List.flatten (List.map pi1 bl)) in (try List.index Names.Name.equal (snd x) ids - with Not_found -> error "No such fix variable.") - | _ -> error "Cannot guess decreasing argument of fix." in + with Not_found -> user_err Pp.(str "No such fix variable.")) + | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in (id,n, CAst.make ~loc @@ CProdN(bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = @@ -152,7 +152,7 @@ let mkTacCase with_evar = function | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then - error "Use of numbers as direct arguments of 'case' is not supported."; + user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported."); TacInductionDestruct (false,with_evar,ic) let rec mkCLambdaN_simple_loc ?loc bll c = diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 75ab1c5ee6..a001c6a2ba 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -348,7 +348,7 @@ type 'a extra_genarg_printer = let bll = List.map (fun (x, _, y) -> x, y) bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a - | _ -> error "Cannot translate fix tactic: not enough products" in + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let pr_ltac_or_var pr = function @@ -1089,7 +1089,7 @@ type 'a extra_genarg_printer = match ty.CAst.v with Glob_term.GProd(na,Explicit,a,b) -> strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b - | _ -> error "Cannot translate fix tactic: not enough products" in + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let raw_printers = @@ -1160,7 +1160,7 @@ type 'a extra_genarg_printer = match Term.kind_of_term ty with Term.Prod(na,a,b) -> strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b - | _ -> error "Cannot translate fix tactic: not enough products" in + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let pr_atomic_tactic_level env sigma n t = @@ -1210,7 +1210,7 @@ let declare_extra_genarg_pprule wit (h : 'c extra_genarg_printer) = begin match wit with | ExtraArg s -> () - | _ -> error "Can declare a pretty-printing rule only for extra argument types." + | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in let g x = diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e8c9f4ebaa..966b11d0e7 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)))) @@ -241,7 +235,7 @@ end) = struct let liftarg = mkLambda (na, ty, arg) in let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs - else error "build_signature: no constraint can apply on a dependent argument" + else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument") | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products") | _, [] -> (match finalcstr with @@ -478,7 +472,7 @@ type hypinfo = { let get_symmetric_proof b = if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof -let error_no_relation () = error "Cannot find a relation to rewrite." +let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.") let rec decompose_app_rel env evd t = (** Head normalize for compatibility with the old meta mechanism *) @@ -531,7 +525,7 @@ let decompose_applied_relation env sigma (c,l) = let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *) match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with | Some c -> c - | None -> error "Cannot find an homogeneous relation to rewrite." + | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.") let rewrite_db = "rewrite" @@ -837,7 +831,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev sigargs, r.rew_to :: typeargs') | None -> if not (Option.is_empty y) then - error "Cannot rewrite inside dependent arguments of a function"; + user_err Pp.(str "Cannot rewrite inside dependent arguments of a function"); x :: acc, x :: subst, evars, sigargs, x :: typeargs') ([], [], evars, sigargs, []) args args' in @@ -1425,7 +1419,7 @@ module Strategies = let unfolded = try Tacred.try_red_product env sigma c with e when CErrors.noncritical e -> - error "fold: the term is not unfoldable !" + user_err Pp.(str "fold: the term is not unfoldable !") in try let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in @@ -2204,7 +2198,7 @@ let setoid_symmetry_in id = let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> let l,res = split_last_two (y::z) in x::l, res - | _ -> error "Cannot find an equivalence relation to rewrite." + | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.") in let others,(c1,c2) = split_last_two args in let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 4d7b0f9296..75f89a81e1 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -60,7 +60,7 @@ let get_tacentry n m = else EntryName (rawwit Tacarg.wit_tactic, atactic n) let get_separator = function -| None -> error "Missing separator." +| None -> user_err Pp.(str "Missing separator.") | Some sep -> sep let rec parse_user_entry s sep = @@ -110,7 +110,7 @@ let get_tactic_entry n = else if 1<=n && n<5 then Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) else - error ("Invalid Tactic Notation level: "^(string_of_int n)^".") + user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) (**********************************************************************) (** State of the grammar extensions *) @@ -170,7 +170,7 @@ let add_tactic_entry (kn, ml, tg) state = in let () = if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then - error "Notation for simple tactic must start with an identifier." + user_err Pp.(str "Notation for simple tactic must start with an identifier.") in let map = function | TacTerm s -> GramTerminal s @@ -208,7 +208,7 @@ let interp_prod_item = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names else begin match ArgT.name s with - | None -> error ("Unknown entry "^s^".") + | None -> user_err Pp.(str ("Unknown entry "^s^".")) | Some arg -> arg end | Some n -> @@ -253,8 +253,8 @@ let pprule pa = { let check_key key = if Tacenv.check_alias key then - error "Conflicting tactic notations keys. This can happen when including \ - twice the same module." + user_err Pp.(str "Conflicting tactic notations keys. This can happen when including \ + twice the same module.") let cache_tactic_notation (_, tobj) = let key = tobj.tacobj_key in diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 6c7eb8c899..e431a13bc2 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -252,7 +252,7 @@ and intern_or_and_intro_pattern lf ist = function let intern_or_and_intro_pattern_loc lf ist = function | ArgVar (_,id) as x -> if find_var id ist then x - else error "Disjunctive/conjunctive introduction pattern expected." + else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.") | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l) let intern_intro_pattern_naming_loc lf ist (loc,pat) = diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 053bb6fa13..7497aae3ca 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 632b9dac14..6ba4c0f930 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") @@ -462,7 +464,7 @@ let theoremedeszeros_termes lp = lexico:=true; |7 -> sinfo "ordre lexico computation with sugar, division by pairs"; lexico:=true; - | _ -> error "nsatz: bad parameter" + | _ -> user_err Pp.(str "nsatz: bad parameter") ); let lvar = List.init nvars (fun i -> Printf.sprintf "x%i" (i + 1)) in let lvar = ["a";"b";"c";"d";"e";"f";"g";"h";"i";"j";"k";"l";"m";"n";"o";"p";"q";"r";"s";"t";"u";"v";"w";"x";"y";"z"] @ lvar in @@ -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] @@ -549,5 +551,5 @@ let nsatz_compute t = let lpol = try nsatz t with Ideal.NotInIdeal -> - error "nsatz cannot solve this problem" in + user_err Pp.(str "nsatz cannot solve this problem") in return_term lpol diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 334baec8d5..ee748567b8 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 @@ -456,7 +456,7 @@ let destructurate_prop sigma t = Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) | Var id,[] -> Kvar id | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) - | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal" + | Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") | _ -> Kufo let destructurate_type sigma t = @@ -891,7 +891,7 @@ let rec scalar p n = function (Lazy.force coq_fast_Zmult_assoc_reverse); focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (n*x)) - | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products" + | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") | (Oatom _ as t) -> [], Otimes(t,Oz n) | Oz i -> [focused_simpl p],Oz(n*i) | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |])) @@ -943,7 +943,7 @@ let rec negate p = function [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] (Lazy.force coq_fast_Zopp_mult_distr_r); focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x)) - | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products" + | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") | (Oatom _ as t) -> let r = Otimes(t,Oz(negone)) in [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r @@ -1026,7 +1026,7 @@ let shrink_pair p f1 f2 = | t1,t2 -> begin oprint t1; print_newline (); oprint t2; print_newline (); - flush Pervasives.stdout; error "shrink.1" + flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1") end let reduce_factor p = function @@ -1038,10 +1038,10 @@ let reduce_factor p = function let rec compute = function | Oz n -> n | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2) - | _ -> error "condense.1" + | _ -> CErrors.user_err Pp.(str "condense.1") in [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c)) - | t -> oprint t; error "reduce_factor.1" + | t -> oprint t; CErrors.user_err Pp.(str "reduce_factor.1") let rec condense p = function | Oplus(f1,(Oplus(f2,r) as t)) -> diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 6b711a1761..ce7ffb1e7e 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -35,7 +35,7 @@ let omega_tactic l = | "positive" -> eval_tactic "zify_positive" | "N" -> eval_tactic "zify_N" | "Z" -> eval_tactic "zify_op" - | s -> CErrors.error ("No Omega knowledge base for type "^s)) + | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s))) (Util.List.sort_uniquize String.compare l) in Tacticals.New.tclTHEN diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index c649cfb2c6..7412de1e80 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") @@ -183,7 +184,7 @@ type inversion_scheme = { goal [gl]. This function uses the auxiliary functions [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) -let i_can't_do_that () = error "Quote: not a simple fixpoint" +let i_can't_do_that () = user_err Pp.(str "Quote: not a simple fixpoint") let decomp_term sigma c = EConstr.kind sigma (Termops.strip_outer_cast sigma c) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index a10ce68b4f..fbed1df176 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/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index c2d7d50502..6479c683b2 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -28,7 +28,7 @@ let romega_tactic unsafe l = | "positive" -> eval_tactic "zify_positive" | "N" -> eval_tactic "zify_N" | "Z" -> eval_tactic "zify_op" - | s -> CErrors.error ("No ROmega knowledge base for type "^s)) + | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s))) (Util.List.sort_uniquize String.compare l) in Tacticals.New.tclTHEN diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e566050766..fdcd622994 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1042,5 +1042,5 @@ let total_reflexive_omega_tactic unsafe = let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; resolution unsafe env reified_goal systems_list - with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" + with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") end } diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index d580fde290..1b07a8ca84 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 e20e78b1a7..38f05978db 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -8,7 +8,6 @@ open Ltac_plugin open Pp -open CErrors open Util open Names open Term @@ -32,6 +31,8 @@ open Misctypes open Newring_ast open Proofview.Notations +let error msg = CErrors.user_err Pp.(str msg) + (****************************************************************************) (* controlled reduction *) @@ -46,7 +47,7 @@ let tag_arg tag_rec map subs i c = let global_head_of_constr sigma c = let f, args = decompose_app sigma c in try fst (Termops.global_of_constr sigma f) - with Not_found -> anomaly (str "global_head_of_constr") + with Not_found -> CErrors.anomaly (str "global_head_of_constr") let global_of_constr_nofail c = try global_of_constr c @@ -82,7 +83,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps with Not_found -> - user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") + CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in @@ -229,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) @@ -274,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) @@ -283,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 *) @@ -359,13 +360,13 @@ let find_ring_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - user_err ~hdr:"ring" + CErrors.user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") in List.iter check cl'; (try ring_for_carrier (EConstr.to_constr sigma ty) with Not_found -> - user_err ~hdr:"ring" + CErrors.user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false @@ -852,13 +853,13 @@ let find_field_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - user_err ~hdr:"field" + CErrors.user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") in List.iter check cl'; (try field_for_carrier (EConstr.to_constr sigma ty) with Not_found -> - user_err ~hdr:"field" + CErrors.user_err ~hdr:"field" (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 862e44ccad..6b752fb4b0 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -468,7 +468,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = | Evar (k, _) -> if Evd.mem sigma0 k then KpatEvar k, f, a else if a <> [] then KpatFlex, f, a else - (match p_origin with None -> CErrors.error "indeterminate pattern" + (match p_origin with None -> CErrors.user_err Pp.(str "indeterminate pattern") | Some (dir, rule) -> errorstrm (str "indeterminate " ++ pr_dir_side dir ++ str " in " ++ pr_constr_pat rule)) @@ -1320,7 +1320,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let fill_occ_term env cl occ sigma0 (sigma, t) = try let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in - if sigma' != sigma0 then CErrors.error "matching impacts evars" + if sigma' != sigma0 then CErrors.user_err Pp.(str "matching impacts evars") else cl, (Evd.merge_universe_context sigma' uc, t') with NoMatch -> try let sigma', uc, t' = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e7b17991e3..c2c8065a98 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/constr_matching.ml b/pretyping/constr_matching.ml index edcfa99c86..2cb837ba03 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -220,9 +220,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PSoApp (n,args),m -> let fold (ans, seen) = function | PRel n -> - let () = if Int.Set.mem n seen then error "Non linear second-order pattern" in + let () = if Int.Set.mem n seen then user_err (str "Non linear second-order pattern") in (n :: ans, Int.Set.add n seen) - | _ -> error "Only bound indices allowed in second order pattern matching." + | _ -> user_err (str "Only bound indices allowed in second order pattern matching.") in let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in let frels = free_rels sigma cT in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 42aaf3a227..bf62cea6b6 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 @@ -1051,7 +1076,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with | Some _ -> - error "Cannot force abstraction on identity instance." + user_err Pp.(str "Cannot force abstraction on identity instance.") | None -> make_subst (ctxt',l,occsl) end @@ -1070,7 +1095,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let set_var k = match occs with | Some Locus.AllOccurrences -> mkVar id - | Some _ -> error "Selection of specific occurrences not supported" + | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in @@ -1108,10 +1133,10 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* This is an arbitrary choice *) let evd = Evd.define evk (Constr.mkVar id) evd in match evar_conv_x ts env_evar evd CUMUL idty evty with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> match reconsider_unif_constraints (evar_conv_x ts) evd with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> evd else @@ -1245,7 +1270,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | None -> evd | Some (evk,ev_info,l) -> let rec aux = function - | [] -> error "Unsolvable existential variables." + | [] -> user_err Pp.(str "Unsolvable existential variables.") | a::l -> try let conv_algo = evar_conv_x ts in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 7cee1e8a7e..45857df2ae 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/evarsolve.ml b/pretyping/evarsolve.ml index 4ada91eb59..98e71c7fd9 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1050,7 +1050,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = | None -> None,candidates | Some filter -> restrict_hyps evd evk filter candidates in match candidates,filter with - | UpdateWith [], _ -> error "Not solvable." + | UpdateWith [], _ -> user_err Pp.(str "Not solvable.") | UpdateWith [nc],_ -> let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in raise (EvarSolvedWhileRestricting (evd,mkEvar ev)) @@ -1230,7 +1230,7 @@ let check_evar_instance evd evk1 body conv_algo = (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> error "Ill-typed evar instance" + with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance") in match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with | Success evd -> evd diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 429e5005ec..7f3bafc685 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -97,7 +97,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = and ntypes = mib.mind_ntypes and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in - if j > nconstr then error "Not enough constructors in the type."; + if j > nconstr then user_err Pp.(str "Not enough constructors in the type."); substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1)) (* Number of constructors *) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index e4fbf8d542..211ffbe01e 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -50,9 +50,9 @@ let is_nowhere = function let simple_clause_of enum_hyps cl = let error_occurrences () = - CErrors.error "This tactic does not support occurrences selection" in + CErrors.user_err Pp.(str "This tactic does not support occurrences selection") in let error_body_selection () = - CErrors.error "This tactic does not support body selection" in + CErrors.user_err Pp.(str "This tactic does not support body selection") in let hyps = match cl.onhyps with | None -> diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0228f63cdc..afaa20b6f6 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -383,7 +383,7 @@ let native_norm env sigma c ty = let c = EConstr.Unsafe.to_constr c in let ty = EConstr.Unsafe.to_constr ty in if Coq_config.no_native_compiler then - error "Native_compute reduction has been disabled at configure time." + user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else let penv = Environ.pre_env env in (* diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index a8012d35f8..1c8ad0cddd 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -230,7 +230,7 @@ let instantiate_pattern env sigma lvar c = error_instantiate_pattern id (List.subtract Id.equal ctx vars) with Not_found (* Map.find failed *) -> x) - | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.") + | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.") | c -> map_pattern_with_binders (fun id vars -> id::vars) aux vars c in aux [] c diff --git a/pretyping/program.ml b/pretyping/program.ml index de485dbe84..8769c5659e 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/pretyping/redops.ml b/pretyping/redops.ml index 7d65925e57..8e190f40b9 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -20,13 +20,13 @@ let make_red_flag l = | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> if red.rDelta then - CErrors.error - "Cannot set both constants to unfold and constants not to unfold"; + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l } lf | FDeltaBut l :: lf -> if red.rConst <> [] && not red.rDelta then - CErrors.error - "Cannot set both constants to unfold and constants not to unfold"; + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l; rDelta = true } lf diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 117ed338ee..e7c9635829 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1219,7 +1219,7 @@ let clos_norm_flags flgs env sigma t = EConstr.of_constr (CClosure.norm_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let clos_whd_flags flgs env sigma t = try @@ -1227,7 +1227,7 @@ let clos_whd_flags flgs env sigma t = EConstr.of_constr (CClosure.whd_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 67221046bd..3d41d2ddd5 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -858,7 +858,7 @@ let try_red_product env sigma c = let red_product env sigma c = try try_red_product env sigma c - with Redelimination -> error "No head constant to reduce." + with Redelimination -> user_err (str "No head constant to reduce.") (* (* This old version of hnf uses betadeltaiota instead of itself (resp @@ -1080,7 +1080,7 @@ let unfold env sigma name c = if is_evaluable env name then clos_norm_flags (unfold_red name) env sigma c else - error (string_of_evaluable_ref env name^" is opaque.") + user_err Pp.(str (string_of_evaluable_ref env name^" is opaque.")) (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. @@ -1090,7 +1090,7 @@ let unfoldoccs env sigma (occs,name) c = let unfo nowhere_except_in locs = let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in if Int.equal nbocc 1 then - error ((string_of_evaluable_ref env name)^" does not occur."); + user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur.")); let rest = List.filter (fun o -> o >= nbocc) locs in let () = match rest with | [] -> () @@ -1112,7 +1112,7 @@ let unfoldn loccname env sigma c = let fold_one_com com env sigma c = let rcom = try red_product env sigma com - with Redelimination -> error "Not reducible." in + with Redelimination -> user_err Pp.(str "Not reducible.") in (* Reason first on the beta-iota-zeta normal form of the constant as unfold produces it, so that the "unfold f; fold f" configuration works to refold fix expressions *) @@ -1147,7 +1147,7 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in let na = named_hd env sigma ta Anonymous in - if occur_meta sigma ta then error "Cannot find a type for the generalisation."; + if occur_meta sigma ta then user_err Pp.(str "Cannot find a type for the generalisation."); if occur_meta sigma a then mkLambda (na,ta,c), sigma else diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 919e95a8ee..d7b4842810 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -422,7 +422,7 @@ let add_class cl = match inst with | Some (Backward, info) -> (match body with - | None -> CErrors.error "Non-definable projection can not be declared as a subinstance" + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") | Some b -> declare_instance (Some info) false (ConstRef b)) | _ -> ()) cl.cl_projs diff --git a/pretyping/unification.ml b/pretyping/unification.ml index cac6c50572..d1643a8c7d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1250,7 +1250,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c = | Prod (_,c1,c2) -> let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' - | _ -> error "Apply_Head_Then" + | _ -> user_err Pp.(str "Apply_Head_Then") in apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd @@ -1516,7 +1516,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 = let iter_fail f a = let n = Array.length a in let rec ffail i = - if Int.equal i n then error "iter_fail" + if Int.equal i n then user_err Pp.(str "iter_fail") else try f a.(i) with ex when precatchable_exception ex -> ffail (i+1) @@ -1754,8 +1754,8 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = w_typed_unify_array env evd flags f1 l1 f2 l2,cl else w_typed_unify env evd CONV flags op cl,cl with ex when Pretype_errors.unsatisfiable_exception ex -> - bestexn := Some ex; error "Unsat") - else error "Bound 1" + bestexn := Some ex; user_err Pp.(str "Unsat")) + else user_err Pp.(str "Bound 1") with ex when precatchable_exception ex -> (match EConstr.kind evd cl with | App (f,args) -> @@ -1804,7 +1804,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = with ex when precatchable_exception ex -> matchrec c) - | _ -> error "Match_subterm")) + | _ -> user_err Pp.(str "Match_subterm"))) in try matchrec cl with ex when precatchable_exception ex -> @@ -1820,7 +1820,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = let (evd,c as a) = a () in if List.exists (fun (evd',c') -> EConstr.eq_constr evd' c c') b then b else a :: b in - let fail str _ = error str in + let fail str _ = user_err (Pp.str str) in let bind f g a = let a1 = try f a with ex @@ -1956,7 +1956,7 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 = | _, Meta p2 -> (* Find the predicate *) secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2) - | _ -> error "w_unify2" + | _ -> user_err Pp.(str "w_unify2") (* The unique unification algorithm works like this: If the pattern is flexible, and the goal has a lambda-abstraction at the head, then diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 74998349be..b08666483e 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -355,7 +355,7 @@ and nf_cofix env sigma cf = let cbv_vm env sigma c t = if Termops.occur_meta_or_existential sigma c then - CErrors.error "vm_compute does not support existential variables."; + CErrors.user_err Pp.(str "vm_compute does not support existential variables."); (** This evar-normalizes terms beforehand *) let c = EConstr.to_constr sigma c in let t = EConstr.to_constr sigma t in diff --git a/printing/pputils.ml b/printing/pputils.ml index d1ba1a4a10..99d07601c4 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -96,7 +96,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l) | Red true -> - CErrors.error "Shouldn't be accessible from user." + CErrors.user_err Pp.(str "Shouldn't be accessible from user.") | ExtraRedExpr s -> str s | CbvVm o -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 70de65acdc..0f7da36133 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -716,7 +716,7 @@ let read_sec_context r = | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | (_,Lib.ClosedSection _)::rest -> - error "Cannot print the contents of a closed section." + user_err Pp.(str "Cannot print the contents of a closed section.") (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest @@ -765,7 +765,7 @@ let print_opaque_name qid = if Declareops.constant_has_body cb then print_constant_with_infos cst else - error "Not a defined constant." + user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> diff --git a/printing/printer.ml b/printing/printer.ml index d4f7afb38c..ebe68680fb 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -566,7 +566,7 @@ let pr_selected_subgoal name sigma g = let default_pr_subgoal n sigma = let rec prrec p = function - | [] -> error "No such goal." + | [] -> user_err Pp.(str "No such goal.") | g::rest -> if Int.equal p 1 then pr_selected_subgoal (int n) sigma g @@ -828,7 +828,7 @@ let pr_goal_by_id id = Proof.in_proof p (fun sigma -> let g = Evd.evar_key id sigma in pr_selected_subgoal (pr_id id) sigma g) - with Not_found -> error "No such goal." + with Not_found -> user_err Pp.(str "No such goal.") let pr_goal_by_uid uid = let p = Proof_global.give_me_the_proof () in @@ -839,7 +839,7 @@ let pr_goal_by_uid uid = in try Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;}) - with Not_found -> error "Invalid goal identifier." + with Not_found -> user_err Pp.(str "Invalid goal identifier.") (* Elementary tactics *) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 9e0a2a03eb..33a86402ef 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -163,7 +163,7 @@ let error_incompatible_inst clenv mv = let clenv_assign mv rhs clenv = let rhs_fls = mk_freelisted rhs in if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then - error "clenv_assign: circularity in unification"; + user_err Pp.(str "clenv_assign: circularity in unification"); try if meta_defined clenv.evd mv then if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then @@ -174,7 +174,7 @@ let clenv_assign mv rhs clenv = let st = (Conv,TypeNotProcessed) in {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd} with Not_found -> - error "clenv_assign: undefined meta" + user_err Pp.(str "clenv_assign: undefined meta") diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index b9c9257969..b1fe128a24 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -39,11 +39,11 @@ let define_and_solve_constraints evk c env evd = pbs with | Success evd -> evd - | UnifFailure _ -> error "Instance does not satisfy the constraints." + | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.") let w_refine (evk,evi) (ltac_var,rawc) sigma = if Evd.is_defined sigma evk then - error "Instantiate called on already-defined evar"; + user_err Pp.(str "Instantiate called on already-defined evar"); let env = Evd.evar_filtered_env evi in let sigma',typed_c = let flags = { diff --git a/proofs/logic.ml b/proofs/logic.ml index 54345abd97..cd2cfbd32f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -141,7 +141,7 @@ let occur_vars_in_decl env sigma hyps d = let reorder_context env sigma sign ord = let ords = List.fold_right Id.Set.add ord Id.Set.empty in if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then - error "Order list has duplicates"; + user_err Pp.(str "Order list has duplicates"); let rec step ord expected ctxt_head moved_hyps ctxt_tail = match ord with | [] -> List.rev ctxt_tail @ ctxt_head diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 92b4e788a2..aaceb7b762 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -71,7 +71,7 @@ let get_universe_binders () = exception NoSuchGoal let _ = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.error "No such goal." + | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end let get_nth_V82_goal i = @@ -87,12 +87,12 @@ let get_goal_context_gen i = let get_goal_context i = try get_goal_context_gen i - with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." - | NoSuchGoal -> CErrors.error "No such goal." + with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") + | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") let get_current_goal_context () = try get_goal_context_gen 1 - with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." + with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, there is no accessible evar either *) @@ -143,7 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) with - Proof_global.NoCurrentProof -> CErrors.error "No focused proof" + Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) diff --git a/proofs/proof.ml b/proofs/proof.ml index b2103489a7..2aa620c1da 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -66,14 +66,14 @@ exception FullyUnfocused let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - CErrors.error "This proof is focused, but cannot be unfocused this way" + CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way") | NoSuchGoals (i,j) when Int.equal i j -> CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> CErrors.user_err ~hdr:"Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) - | FullyUnfocused -> CErrors.error "The proof is not focused" + | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") | _ -> raise CErrors.Unhandled end @@ -301,10 +301,10 @@ exception HasShelvedGoals exception HasGivenUpGoals exception HasUnresolvedEvar let _ = CErrors.register_handler begin function - | UnfinishedProof -> CErrors.error "Some goals have not been solved." - | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf." - | HasGivenUpGoals -> CErrors.error "Some goals have been given up." - | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated." + | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.") + | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.") + | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.") + | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.") | _ -> raise CErrors.Unhandled end @@ -420,9 +420,9 @@ module V82 = struct let evl = Evarutil.non_instantiated sigma in let evl = Evar.Map.bindings evl in if (n <= 0) then - CErrors.error "incorrect existential variable index" + CErrors.user_err Pp.(str "incorrect existential variable index") else if CList.length evl < n then - CErrors.error "not so many uninstantiated existential variables" + CErrors.user_err Pp.(str "not so many uninstantiated existential variables") else CList.nth evl (n-1) in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 95aee72cb5..4d2f534a76 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -36,7 +36,7 @@ let proof_modes = Hashtbl.create 6 let find_proof_mode n = try Hashtbl.find proof_modes n with Not_found -> - CErrors.error (Format.sprintf "No proof mode named \"%s\"." n) + CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n)) let register_proof_mode ({name = n} as m) = Hashtbl.add proof_modes n (CEphemeron.create m) @@ -124,13 +124,13 @@ let push a l = l := a::!l; exception NoSuchProof let _ = CErrors.register_handler begin function - | NoSuchProof -> CErrors.error "No such proof." + | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") | _ -> raise CErrors.Unhandled end exception NoCurrentProof let _ = CErrors.register_handler begin function - | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)." + | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end @@ -299,7 +299,7 @@ let set_used_variables l = | [] -> raise NoCurrentProof | p :: rest -> if not (Option.is_empty p.section_vars) then - CErrors.error "Used section variables can be declared only once"; + CErrors.user_err Pp.(str "Used section variables can be declared only once"); pstates := { p with section_vars = Some ctx} :: rest; ctx, to_clear @@ -637,7 +637,7 @@ module Bullet = struct current_behavior := try Hashtbl.find behaviors n with Not_found -> - CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") + CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")) end }) @@ -687,9 +687,9 @@ let parse_goal_selector = function let err_msg = "The default selector must be \"all\" or a natural number." in begin try let i = int_of_string i in - if i < 0 then CErrors.error err_msg; + if i < 0 then CErrors.user_err Pp.(str err_msg); Vernacexpr.SelectNth i - with Failure _ -> CErrors.error err_msg + with Failure _ -> CErrors.user_err Pp.(str err_msg) end let _ = diff --git a/stm/stm.ml b/stm/stm.ml index 7999178012..b98cb312ed 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -127,8 +127,9 @@ type qed_t = { brname : Vcs_.Branch.t; brinfo : branch_type Vcs_.branch_info } -type seff_t = aast option +type seff_t = ReplayCommand of aast | CherryPickEnv type alias_t = Stateid.t * aast + type transaction = | Cmd of cmd_t | Fork of fork_t @@ -140,7 +141,7 @@ type step = [ `Cmd of cmd_t | `Fork of fork_t * Stateid.t option | `Qed of qed_t * Stateid.t - | `Sideff of [ `Ast of aast * Stateid.t | `Id of Stateid.t ] + | `Sideff of seff_t * Stateid.t | `Alias of alias_t ] type visit = { step : step; next : Stateid.t } @@ -239,11 +240,11 @@ end = struct (* {{{ *) | [p, Noop; n, Fork x] -> { step = `Fork (x,Some p); next = n } | [n, Qed x; p, Noop] | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n } - | [n, Sideff None; p, Noop] - | [p, Noop; n, Sideff None]-> { step = `Sideff (`Id p); next = n } - | [n, Sideff (Some x); p, Noop] - | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n } - | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n} + | [n, Sideff CherryPickEnv; p, Noop] + | [p, Noop; n, Sideff CherryPickEnv]-> { step = `Sideff (CherryPickEnv, p); next = n } + | [n, Sideff (ReplayCommand x); p, Noop] + | [p, Noop; n, Sideff (ReplayCommand x)]-> { step = `Sideff(ReplayCommand x,p); next = n } + | [n, Sideff (ReplayCommand x)]-> {step = `Sideff(ReplayCommand x, Stateid.dummy); next=n} | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id)) with Not_found -> raise Expired @@ -305,7 +306,7 @@ module VCS : sig val proof_nesting : unit -> int val checkout_shallowest_proof_branch : unit -> unit - val propagate_sideff : replay:aast option -> unit + val propagate_sideff : action:seff_t -> unit val gc : unit -> unit @@ -338,10 +339,10 @@ end = struct (* {{{ *) let string_of_transaction = function | Cmd { cast = t } | Fork (t, _,_,_) -> (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") - | Sideff (Some t) -> + | Sideff (ReplayCommand t) -> sprintf "Sideff(%s)" (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") - | Sideff None -> "EnvChange" + | Sideff CherryPickEnv -> "EnvChange" | Noop -> " " | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id) | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in @@ -514,11 +515,11 @@ end = struct (* {{{ *) Proof_global.disactivate_current_proof_mode () (* copies the transaction on every open branch *) - let propagate_sideff ~replay:t = + let propagate_sideff ~action = List.iter (fun b -> checkout b; let id = new_node () in - merge id ~ours:(Sideff t) ~into:b Branch.master) + merge id ~ours:(Sideff action) ~into:b Branch.master) (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) let visit id = Vcs_aux.visit !vcs id @@ -529,8 +530,8 @@ end = struct (* {{{ *) match visit id with | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n | { next = n; step = `Alias x } -> (id,Alias x) :: aux n - | { next = n; step = `Sideff (`Ast (x,_)) } -> - (id,Sideff (Some x)) :: aux n + | { next = n; step = `Sideff (ReplayCommand x,_) } -> + (id,Sideff (ReplayCommand x)) :: aux n | _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^ " to "^Stateid.to_string block_stop)) in aux block_stop @@ -913,9 +914,9 @@ let get_script prf = match view.step with | `Fork((_,_,_,ns), _) when test ns -> acc | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof - | `Sideff (`Ast (x,_)) -> + | `Sideff (ReplayCommand x,_) -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Sideff (`Id id) -> find acc id + | `Sideff (CherryPickEnv, id) -> find acc id | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next | `Cmd _ -> find acc view.next @@ -1171,7 +1172,7 @@ let register_proof_block_delimiter name static dynamic = let mk_doc_node id = function | { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac -> Some { indentation; ast = expr; id } - | { step = `Sideff (`Ast ({ indentation; expr }, _)); next } -> + | { step = `Sideff (ReplayCommand { indentation; expr }, _); next } -> Some { indentation; ast = expr; id } | _ -> None let prev_node { id } = @@ -1537,7 +1538,7 @@ end = struct (* {{{ *) | { step = `Cmd { cast = { loc } } } | { step = `Fork (( { loc }, _, _, _), _) } | { step = `Qed ( { qast = { loc } }, _) } - | { step = `Sideff (`Ast ( { loc }, _)) } -> + | { step = `Sideff (ReplayCommand { loc }, _) } -> let start, stop = Option.cata Loc.unloc (0,0) loc in msg_error Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ @@ -2003,10 +2004,10 @@ let collect_proof keep cur hd brkind id = let rec collect last accn id = let view = VCS.visit id in match view.step with - | (`Sideff (`Ast(x,_)) | `Cmd { cast = x }) + | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x }) when too_complex_to_delegate x -> `Sync(no_name,None,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next - | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next + | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) | `Alias _ -> `Sync (no_name,None,`Alias) | `Fork((_,_,_,_::_::_), _) -> @@ -2305,10 +2306,10 @@ let known_state ?(redefine_qed=false) ~cache id = ), (if redefine_qed then `No else `Yes), true in aux (collect_proof keep (view.next, x) brname brinfo eop) - | `Sideff (`Ast (x,_)) -> (fun () -> + | `Sideff (ReplayCommand x,_) -> (fun () -> reach view.next; stm_vernac_interp id x; update_global_env () ), cache, true - | `Sideff (`Id origin) -> (fun () -> + | `Sideff (CherryPickEnv, origin) -> (fun () -> reach view.next; inject_non_pstate (pure_cherry_pick_non_pstate view.next origin); ), cache, true @@ -2429,7 +2430,7 @@ let merge_proof_branch ~valid ?id qast keep brname = let id = VCS.new_node ?id () in VCS.merge id ~ours:(Qed (qed None)) brname; VCS.delete_branch brname; - VCS.propagate_sideff ~replay:None; + VCS.propagate_sideff ~action:CherryPickEnv; `Ok | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> let ofp = @@ -2600,10 +2601,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) VCS.commit id (mkTransCmd x l in_proof `MainQueue); (* We can't replay a Definition since universes may be differently * inferred. This holds in Coq >= 8.5 *) - let replay = match x.expr with - | VernacDefinition(_, _, DefineBody _) -> None - | _ -> Some x in - VCS.propagate_sideff ~replay; + let action = match x.expr with + | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv + | _ -> ReplayCommand x in + VCS.propagate_sideff ~action; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); `Ok @@ -2634,7 +2635,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) end else begin VCS.commit id (mkTransCmd x [] in_proof `MainQueue); (* We hope it can be replayed, but we can't really know *) - VCS.propagate_sideff ~replay:(Some x); + VCS.propagate_sideff ~action:(ReplayCommand x); VCS.checkout_shallowest_proof_branch (); end in State.define ~safe_id:head_id ~cache:`Yes step id; @@ -2811,7 +2812,7 @@ let edit_at id = if Stateid.equal tip Stateid.initial then tip else match VCS.visit tip with | { step = (`Fork _ | `Qed _) } -> tip - | { step = `Sideff (`Ast(_,id)) } -> id + | { step = `Sideff (ReplayCommand _,id) } -> id | { step = `Sideff _ } -> tip | { next } -> master_for_br root next in let reopen_branch start at_id mode qed_id tip old_branch = diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index b2ea3341b4..9f50ab589d 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -24,7 +24,7 @@ end module Pool = Map.Make(IntOT) let schedule_vio_checking j fs = - if j < 1 then CErrors.error "The number of workers must be bigger than 0"; + if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in List.iter (fun f -> let f = @@ -98,7 +98,7 @@ let schedule_vio_checking j fs = exit !rc let schedule_vio_compilation j fs = - if j < 1 then CErrors.error "The number of workers must be bigger than 0"; + if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in List.iter (fun f -> let f = diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 918371d55e..46d66b9d06 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -938,7 +938,7 @@ module V85 = struct | Some (evd', fk) -> if unique then (match get_result (fk NotApplicable) with - | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions" + | Some (evd'', fk') -> user_err Pp.(str "Typeclass resolution gives multiple solutions") | None -> evd') else evd' diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 768d6860dc..fe44559ed8 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/eauto.ml b/tactics/eauto.ml index e87368dec6..986f531397 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -62,7 +62,7 @@ let registered_e_assumption = let first_goal gls = let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in - if List.is_empty gl then error "first_goal"; + if List.is_empty gl then user_err Pp.(str "first_goal"); { Evd.it = List.hd gl; Evd.sigma = sig_0; } (* tactic -> tactic_list : Apply a tactic to the first goal in the list *) @@ -73,7 +73,7 @@ let apply_tac_list tac glls = | (g1::rest) -> let gl = apply_sig_tac sigr tac g1 in repackage sigr (gl@rest) - | _ -> error "apply_tac_list" + | _ -> user_err Pp.(str "apply_tac_list") let one_step l gl = [Proofview.V82.of_tactic Tactics.intro] @@ -82,7 +82,7 @@ let one_step l gl = @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl)) let rec prolog l n gl = - if n <= 0 then error "prolog - failure"; + if n <= 0 then user_err Pp.(str "prolog - failure"); let prol = (prolog l (n-1)) in (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl @@ -402,7 +402,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl = s.tacres with Not_found -> pr_info_nop d; - error "eauto: search failed" + user_err Pp.(str "eauto: search failed") (* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) (* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 641929a77b..bda25d7f02 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/eqschemes.ml b/tactics/eqschemes.ml index d023b45682..bcd31cb7e7 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -103,7 +103,7 @@ let get_coq_eq ctx = (Universes.fresh_inductive_instance (Global.env ()) eq) in mkIndU eq, mkConstructUi (eq,1), ctx with Not_found -> - error "eq not found." + user_err Pp.(str "eq not found.") let univ_of_eq env eq = let eq = EConstr.of_constr eq in @@ -120,6 +120,8 @@ let univ_of_eq env eq = (* in which case, a symmetry lemma is definable *) (**********************************************************************) +let error msg = user_err Pp.(str msg) + let get_sym_eq_data env (ind,u) = let (mib,mip as specif) = lookup_mind_specif env ind in if not (Int.equal (Array.length mib.mind_packets) 1) || diff --git a/tactics/equality.ml b/tactics/equality.ml index 70d6fe90c5..e6278943df 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -164,7 +164,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in let (equiv, args) = decompose_app_vect sigma (Clenv.clenv_type eqclause) in let arglen = Array.length args in - let () = if arglen < 2 then error "The term provided is not an applied relation." in + let () = if arglen < 2 then user_err Pp.(str "The term provided is not an applied relation.") in let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = @@ -441,7 +441,7 @@ let adjust_rewriting_direction args lft2rgt = (* equality to a constant, like in eq_true *) (* more natural to see -> as the rewriting to the constant *) if not lft2rgt then - error "Rewriting non-symmetric equality not allowed from right-to-left."; + user_err Pp.(str "Rewriting non-symmetric equality not allowed from right-to-left."); None | _ -> (* other equality *) @@ -865,7 +865,7 @@ let descend_then env sigma head dirn = let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> - error "Cannot project on an inductive type derived from a dependency." in + user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") in let indp,_ = (dest_ind_family indf) in let ind, _ = check_privacy env indp in let (mib,mip) = lookup_mind_specif env ind in @@ -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 | [] -> @@ -1202,7 +1202,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in dflt with Evarconv.UnableToUnify _ -> - error "Cannot solve a unification problem." + user_err Pp.(str "Cannot solve a unification problem.") else let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with | (_sigS,[a;p]) -> (a, p) @@ -1219,7 +1219,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let exist_term = EConstr.of_constr exist_term in applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) else - error "Cannot solve a unification problem." + user_err Pp.(str "Cannot solve a unification problem.") | None -> (* This at least happens if what has been detected as a dependency is not one; use an evasive error message; @@ -1227,7 +1227,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = tried in the first place in make_iterated_tuple instead of approximatively computing the free rels; then unsolved evars would mean not binding rel *) - error "Cannot solve a unification problem." + user_err Pp.(str "Cannot solve a unification problem.") in let scf = sigrec_clausal_form siglen ty in !evdref, Evarutil.nf_evar !evdref scf @@ -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 @@ -1887,7 +1886,7 @@ let cond_eq_term c t gl = let rewrite_assumption_cond cond_eq_term cl = let rec arec hyps gl = match hyps with - | [] -> error "No such assumption." + | [] -> user_err Pp.(str "No such assumption.") | hyp ::rest -> let id = NamedDecl.get_id hyp in begin diff --git a/tactics/hints.ml b/tactics/hints.ml index e6edae7ef6..48a7b3f75c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -59,7 +59,7 @@ let head_constr_bound sigma t = | _ -> raise Bound let head_constr sigma c = - try head_constr_bound sigma c with Bound -> error "Bound head variable." + try head_constr_bound sigma c with Bound -> user_err Pp.(str "Bound head variable.") let decompose_app_bound sigma t = let t = strip_outer_cast sigma t in @@ -167,7 +167,7 @@ let write_warn_hint = function | "Lax" -> warn_hint := `LAX | "Warn" -> warn_hint := `WARN | "Strict" -> warn_hint := `STRICT -| _ -> error "Only the following flags are accepted: Lax, Warn, Strict." +| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.") let _ = Goptions.declare_string_option @@ -767,7 +767,7 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with let try_head_pattern c = try head_pattern_bound c - with BoundPattern -> error "Bound head variable." + with BoundPattern -> user_err Pp.(str "Bound head variable.") let with_uid c = { obj = c; uid = fresh_key () } @@ -980,8 +980,8 @@ let get_db dbname = let add_hint dbname hintlist = let check (_, h) = let () = if KNmap.mem h.code.uid !statustable then - error "Conflicting hint keys. This can happen when including \ - twice the same module." + user_err Pp.(str "Conflicting hint keys. This can happen when including \ + twice the same module.") in statustable := KNmap.add h.code.uid false !statustable in @@ -1246,10 +1246,10 @@ let prepare_hint check (poly,local) env init (sigma,c) = let t = Evarutil.nf_evar sigma (existential_type sigma ev) in let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in if not (closed0 sigma c) then - error "Hints with holes dependent on a bound variable not supported."; + user_err Pp.(str "Hints with holes dependent on a bound variable not supported."); if occur_existential sigma t then (* Not clever enough to construct dependency graph of evars *) - error "Not clever enough to deal with evars dependent in other evars."; + user_err Pp.(str "Not clever enough to deal with evars dependent in other evars."); raise (Found (c,t)) | _ -> EConstr.iter sigma find_next_evar c in let rec iter c = @@ -1322,7 +1322,7 @@ let interp_hints poly = let add_hints local dbnames0 h = if String.List.mem "nocore" dbnames0 then - error "The hint database \"nocore\" is meant to stay empty."; + user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in let env = Global.env() in let sigma = Evd.from_env env in @@ -1471,7 +1471,7 @@ let pr_applicable_hint () = let pts = get_pftreestate () in let glss = Proof.V82.subgoals pts in match glss.Evd.it with - | [] -> CErrors.error "No focused goal." + | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index dce98eed74..fd5eabe648 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -460,7 +460,7 @@ let find_this_eq_data_decompose gl eqn = let eq_args = try extract_eq_args gl eq_args with PatternMatchingFailure -> - error "Don't know what to do with JMeq on arguments not of same type." in + user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) let match_eq_nf gls eqn (ref, hetero) = @@ -477,7 +477,7 @@ let dest_nf_eq gls eqn = try snd (first_match (match_eq_nf gls eqn) equalities) with PatternMatchingFailure -> - error "Not an equality." + user_err Pp.(str "Not an equality.") (*** Sigma-types *) diff --git a/tactics/inv.ml b/tactics/inv.ml index 5c4b73a622..b951e7ceba 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -292,27 +292,27 @@ let error_too_many_names pats = let get_names (allow_conj,issimple) (loc, pat as x) = match pat with | IntroNaming IntroAnonymous | IntroForthcoming _ -> - error "Anonymous pattern not allowed for inversion equations." + user_err Pp.(str "Anonymous pattern not allowed for inversion equations.") | IntroNaming (IntroFresh _) -> - error "Fresh pattern not allowed for inversion equations." + user_err Pp.(str "Fresh pattern not allowed for inversion equations.") | IntroAction IntroWildcard -> - error "Discarding pattern not allowed for inversion equations." + user_err Pp.(str "Discarding pattern not allowed for inversion equations.") | IntroAction (IntroRewrite _) -> - error "Rewriting pattern not allowed for inversion equations." + user_err Pp.(str "Rewriting pattern not allowed for inversion equations.") | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, []) | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l) | IntroOrPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l ])) when allow_conj -> (Some id,l) | IntroAction (IntroOrAndPattern (IntroAndPattern _)) -> if issimple then - error"Conjunctive patterns not allowed for simple inversion equations." + user_err Pp.(str"Conjunctive patterns not allowed for simple inversion equations.") else - error"Nested conjunctive patterns not allowed for inversion equations." + user_err Pp.(str"Nested conjunctive patterns not allowed for inversion equations.") | IntroAction (IntroInjection l) -> - error "Injection patterns not allowed for inversion equations." + user_err Pp.(str "Injection patterns not allowed for inversion equations.") | IntroAction (IntroOrAndPattern (IntroOrPattern _)) -> - error "Disjunctive patterns not allowed for inversion equations." + user_err Pp.(str "Disjunctive patterns not allowed for inversion equations.") | IntroAction (IntroApplyOn (c,pat)) -> - error "Apply patterns not allowed for inversion equations." + user_err Pp.(str "Apply patterns not allowed for inversion equations.") | IntroNaming (IntroIdentifier id) -> (Some id,[x]) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index fe9cb123ce..c495b5ece2 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -69,7 +69,7 @@ let tclTHENSEQ = tclTHENLIST let nthDecl m gl = try List.nth (pf_hyps gl) (m-1) - with Failure _ -> error "No such assumption." + with Failure _ -> user_err Pp.(str "No such assumption.") let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) @@ -80,7 +80,7 @@ let lastHyp gl = nthHyp 1 gl let nLastDecls n gl = try List.firstn n (pf_hyps gl) - with Failure _ -> error "Not enough hypotheses in the goal." + with Failure _ -> user_err Pp.(str "Not enough hypotheses in the goal.") let nLastHypsId n gl = List.map (NamedDecl.get_id) (nLastDecls n gl) let nLastHyps n gl = List.map mkVar (nLastHypsId n gl) @@ -533,11 +533,11 @@ module New = struct let hyps = Proofview.Goal.hyps gl in try List.nth hyps (m-1) - with Failure _ -> CErrors.error "No such assumption." + with Failure _ -> CErrors.user_err Pp.(str "No such assumption.") let nLastDecls gl n = try List.firstn n (Proofview.Goal.hyps gl) - with Failure _ -> error "Not enough hypotheses in the goal." + with Failure _ -> CErrors.user_err Pp.(str "Not enough hypotheses in the goal.") let nthHypId m gl = (** We only use [id] *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c713a31fa3..7e8cb4e632 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -195,6 +195,7 @@ let introduction ?(check=true) id = end } let refine = Tacmach.refine +let error msg = CErrors.user_err Pp.(str msg) let convert_concl ?(check=true) ty k = Proofview.Goal.enter { enter = begin fun gl -> @@ -3520,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 570bf32227..285460762b 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 diff --git a/test-suite/coq-makefile/arg/run.sh b/test-suite/coq-makefile/arg/run.sh index 28b9bcb969..e98da17c78 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 ccb348c6fa..28d9878f9b 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 e071f1db7a..d6bb52bb4a 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 e071f1db7a..d6bb52bb4a 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 db11601132..ea5792a937 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 45f2269113..214a9d5b28 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 9b89e5b6e9..752c0c2cea 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 418a2fb775..f6fb3bcb42 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 418a2fb775..f6fb3bcb42 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 a24a8a3cf7..863c39f500 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 097bd6398a..bc9f846dda 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 4b471bcb80..2ea3deffb7 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 684e0ece82..24ef8c891b 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 684e0ece82..24ef8c891b 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 684e0ece82..24ef8c891b 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 c952d41a30..c952d41a30 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 d241762791..e525e12086 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 d241762791..e525e12086 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 61025021d0..aaa4194b38 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 0000000000..bf1bf2809d --- /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 0000000000..60faac8dd9 --- /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 5231899c6e..fb064c495f 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/coqdep.ml b/tools/coqdep.ml index 930b092d3b..044399544a 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -495,7 +495,7 @@ let coqdep () = add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); let coqlib = Envars.coqlib () in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 82d3d62b59..e06ef9d765 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/tools/coqmktop.ml b/tools/coqmktop.ml index 7fa8fd58db..defc803381 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -227,7 +227,7 @@ let declare_loading_string () = \n Mltop.set_top\ \n {Mltop.load_obj=\ \n (fun f -> if not (Topdirs.load_file ppf f)\ -\n then CErrors.error (\"Could not load plugin \"^f));\ +\n then CErrors.user_err Pp.(str (\"Could not load plugin \"^f)));\ \n Mltop.use_file=Topdirs.dir_use ppf;\ \n Mltop.add_dir=Topdirs.dir_directory;\ \n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ @@ -257,7 +257,7 @@ let create_tmp_main_file modules = let main () = let (options, userfiles) = parse_args () in (* Directories: *) - let () = Envars.set_coqlib ~fail:CErrors.error in + let () = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)) in let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in (* Which ocaml compiler to invoke *) let prog = if !opt then "opt" else "ocamlc" in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ac1e623d76..7834b5113b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -133,7 +133,7 @@ let set_batch_mode () = batch_mode := true let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) let toplevel_name = ref toplevel_default_name let set_toplevel_name dir = - if Names.DirPath.is_empty dir then error "Need a non empty toplevel module name"; + if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name"); toplevel_name := dir let remove_top_ml () = Mltop.remove () @@ -245,7 +245,7 @@ let compile_files () = let set_emacs () = if not (Option.is_empty !toploop) then - error "Flag -emacs is incompatible with a custom toplevel loop"; + user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); Flags.print_emacs := true; Printer.enable_goal_tags_printing := true; color := `OFF @@ -253,14 +253,14 @@ let set_emacs () = (** Options for CoqIDE *) let set_ideslave () = - if !Flags.print_emacs then error "Flags -ideslave and -emacs are incompatible"; + if !Flags.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); toploop := Some "coqidetop"; Flags.ide_slave := true (** Options for slaves *) let set_toploop name = - if !Flags.print_emacs then error "Flags -toploop and -emacs are incompatible"; + if !Flags.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible"); toploop := Some name (** GC tweaking *) @@ -591,7 +591,7 @@ let parse_args arglist = |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml () |"-emacs-U" -> warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs () - |"-v7" -> error "This version of Coq does not support v7 syntax" + |"-v7" -> user_err Pp.(str "This version of Coq does not support v7 syntax") |"-v8" -> warning "Obsolete option \"-v8\"." |"-lazy-load-proofs" -> warning "Obsolete option \"-lazy-load-proofs\"." |"-dont-load-proofs" -> warning "Obsolete option \"-dont-load-proofs\"." @@ -619,7 +619,7 @@ let init_toplevel arglist = (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); if !print_config then (Envars.print_config stdout; exit (exitcode ())); if !print_tags then (print_style_tags (); exit (exitcode ())); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7e81aa20ad..a61ade7849 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -29,7 +29,7 @@ let checknav_deep (loc, ast) = let disable_drop = function - | Drop -> CErrors.error "Drop is forbidden." + | Drop -> CErrors.user_err Pp.(str "Drop is forbidden.") | e -> e (* Echo from a buffer based on position. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 31d610abda..cf534f13a2 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/classes.ml b/vernac/classes.ml index 5843da31ed..004083dcf9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -353,7 +353,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) (); id) end - else CErrors.error "Unsolved obligations remaining.") + else CErrors.user_err Pp.(str "Unsolved obligations remaining.")) let named_of_rel_context l = let acc, ctx = @@ -379,7 +379,7 @@ let context poly l = let ctx = try named_of_rel_context fullctx with e when CErrors.noncritical e -> - error "Anonymous variables not allowed in contexts." + user_err Pp.(str "Anonymous variables not allowed in contexts.") in let uctx = ref (Evd.universe_context_set !evars) in let fn status (id, b, t) = diff --git a/vernac/command.ml b/vernac/command.ml index 8a9bbb8846..e2ebb4d7fb 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -382,7 +382,7 @@ type structured_inductive_expr = local_binder_expr list * structured_one_inductive_expr list let minductive_message warn = function - | [] -> error "No inductive definition." + | [] -> user_err Pp.(str "No inductive definition.") | [x] -> (pr_id x ++ str " is defined" ++ if warn then str " as a non-primitive record" else mt()) | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ @@ -676,8 +676,8 @@ let extract_params indl = match paramsl with | [] -> anomaly (Pp.str "empty list of inductive types") | params::paramsl -> - if not (List.for_all (eq_local_binders params) paramsl) then error - "Parameters should be syntactically the same for each inductive type."; + if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str + "Parameters should be syntactically the same for each inductive type."); params let extract_inductive indl = @@ -715,9 +715,9 @@ let declare_mutual_inductive_with_eliminations mie pl impls = begin match mie.mind_entry_finite with | BiFinite when is_recursive mie -> if Option.has_some mie.mind_entry_record then - error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command." + user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") else - error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.") + user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) | _ -> () end; let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in @@ -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" @@ -1122,7 +1123,7 @@ let interp_recursive isfix fixl notations = | x , None -> x | Some ls , Some us -> if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then - error "(co)-recursive definitions should all have the same universe binders"; + user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in let ctx = Evd.make_evar_universe_context env all_universes in let evdref = ref (Evd.from_ctx ctx) in @@ -1262,8 +1263,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let extract_decreasing_argument limit = function | (na,CStructRec) -> na | (na,_) when not limit -> na - | _ -> error - "Only structural decreasing is supported for a non-Program Fixpoint" + | _ -> user_err Pp.(str + "Only structural decreasing is supported for a non-Program Fixpoint") let extract_fixpoint_components limit l = let fixl, ntnl = List.split l in @@ -1282,7 +1283,7 @@ let extract_cofixpoint_components l = let out_def = function | Some def -> def - | None -> error "Program Fixpoint needs defined bodies." + | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") let collect_evars_of_term evd c ty = let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml index c6588684a4..f3259f1f3b 100644 --- a/vernac/ind_tables.ml +++ b/vernac/ind_tables.ml @@ -81,7 +81,7 @@ let scheme_object_table = let declare_scheme_object s aux f = let () = if not (Id.is_valid ("ind" ^ s)) then - error ("Illegal induction scheme suffix: " ^ s) + user_err Pp.(str ("Illegal induction scheme suffix: " ^ s)) in let key = if String.is_empty aux then s else aux in try diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index b21e80bef1..f57b1bba01 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -418,7 +418,7 @@ let get_common_underlying_mutual_inductive = function raise (RecursionSchemeError (NotMutualInScheme (ind,ind'))) | [] -> if not (List.distinct_f Int.compare (List.map snd (List.map snd all))) - then error "A type occurs twice"; + then user_err Pp.(str "A type occurs twice"); mind, List.map_filter (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all @@ -429,7 +429,7 @@ let do_scheme l = tried to declare different schemes at once *) if not (List.is_empty ischeme) && not (List.is_empty escheme) then - error "Do not declare equality and induction scheme at the same time." + user_err Pp.(str "Do not declare equality and induction scheme at the same time.") else ( if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme else @@ -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 *) @@ -497,7 +498,7 @@ let do_combined_scheme name schemes = let refe = Ident x in let qualid = qualid_of_reference refe in try Nametab.locate_constant (snd qualid) - with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")) + with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared.")) schemes in let body,typ = build_combined_scheme (Global.env ()) csts in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index c67a3302ff..d6ae0ea86f 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -153,9 +153,9 @@ let find_mutually_recursive_statements thms = (* assume the largest indices as possible *) List.last common_same_indhyp, false, possible_guards | _, [] -> - error + user_err Pp.(str ("Cannot find common (mutual) inductive premises or coinductive" ^ - " conclusions in the statements.") + " conclusions in the statements.")) in (finite,guard,None), ordered_inds @@ -273,7 +273,7 @@ let save_named ?export_seff proof = let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then - error "This command can only be used for unnamed theorem." + user_err Pp.(str "This command can only be used for unnamed theorem.") let save_anonymous ?export_seff proof save_ident = let id,const,(cstrs,pl),do_guard,persistence,hook = proof in @@ -478,10 +478,10 @@ let save_proof ?proof = function match proof with | Some ({ id; entries; persistence = k; universes }, _) -> if List.length entries <> 1 then - error "Admitted does not support multiple statements"; + user_err Pp.(str "Admitted does not support multiple statements"); let { const_entry_secctx; const_entry_type } = List.hd entries in if const_entry_type = None then - error "Admitted requires an explicit statement"; + user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in let ctx = Evd.evar_context_universe_context (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in diff --git a/vernac/locality.ml b/vernac/locality.ml index 03640676e6..a25acb0d34 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -35,9 +35,9 @@ let enforce_locality_full locality_flag local = let local = match locality_flag with | Some false when local -> - CErrors.error "Cannot be simultaneously Local and Global." + CErrors.user_err Pp.(str "Cannot be simultaneously Local and Global.") | Some true when local -> - CErrors.error "Use only prefix \"Local\"." + CErrors.user_err Pp.(str "Use only prefix \"Local\".") | None -> if local then begin warn_deprecated_local_syntax (); @@ -66,7 +66,7 @@ let enforce_locality_exp locality_flag local = | None, Some local -> local | Some b, None -> local_of_bool b | None, None -> Decl_kinds.Global - | Some _, Some _ -> CErrors.error "Local non allowed in this case" + | Some _, Some _ -> CErrors.user_err Pp.(str "Local non allowed in this case") (* For commands whose default is to not discharge but to export: Global in sections forces discharge, Global not in section is the default; @@ -87,8 +87,8 @@ let enforce_section_locality locality_flag local = let make_module_locality = function | Some false -> if Lib.sections_are_opened () then - CErrors.error - "This command does not support the Global option in sections."; + CErrors.user_err Pp.(str + "This command does not support the Global option in sections."); false | Some true -> true | None -> false diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index fb7c729412..42494dd28a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -60,7 +60,7 @@ let pr_entry e = let pr_registered_grammar name = let gram = try Some (String.Map.find name !grammars) with Not_found -> None in match gram with - | None -> error "Unknown or unprintable grammar entry." + | None -> user_err Pp.(str "Unknown or unprintable grammar entry.") | Some entries -> let pr_one (AnyEntry e) = str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++ @@ -107,11 +107,11 @@ let parse_format ((loc, str) : lstring) = if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in let close_box i b = function | a::(_::_ as l) -> push_token (UnpBox (b,a)) l - | _ -> error "Non terminated box in format." in + | _ -> user_err Pp.(str "Non terminated box in format.") in let close_quotation i = if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ') then i+1 - else error "Incorrectly terminated quoted expression." in + else user_err Pp.(str "Incorrectly terminated quoted expression.") in let rec spaces n i = if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1) else n in @@ -119,10 +119,10 @@ let parse_format ((loc, str) : lstring) = if i < String.length str && str.[i] != ' ' then if str.[i] == '\'' && quoted && (i+1 >= String.length str || str.[i+1] == ' ') - then if Int.equal n 0 then error "Empty quoted token." else n + then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n else nonspaces quoted (n+1) (i+1) else - if quoted then error "Spaces are not allowed in (quoted) symbols." + if quoted then user_err Pp.(str "Spaces are not allowed in (quoted) symbols.") else n in let rec parse_non_format i = let n = nonspaces false 0 i in @@ -153,8 +153,8 @@ let parse_format ((loc, str) : lstring) = (* Parse " [ .. ", *) | ' ' | '\'' -> parse_box (fun n -> PpHOVB n) (i+1) - | _ -> error "\"v\", \"hv\", \" \" expected after \"[\" in format." - else error "\"v\", \"hv\" or \" \" expected after \"[\" in format." + | _ -> user_err Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.") + else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.") (* Parse "]" *) | ']' -> ([] :: parse_token (close_quotation (i+1))) @@ -165,7 +165,7 @@ let parse_format ((loc, str) : lstring) = (parse_token (close_quotation (i+n)))) else if Int.equal n 0 then [] - else error "Ending spaces non part of a format annotation." + else user_err Pp.(str "Ending spaces non part of a format annotation.") and parse_box box i = let n = spaces 0 i in close_box i (box n) (parse_token (close_quotation (i+n))) @@ -187,9 +187,9 @@ let parse_format ((loc, str) : lstring) = try if not (String.is_empty str) then match parse_token 0 with | [l] -> l - | _ -> error "Box closed without being opened in format." + | _ -> user_err Pp.(str "Box closed without being opened in format.") else - error "Empty format." + user_err Pp.(str "Empty format.") with reraise -> let (e, info) = CErrors.push reraise in let info = Option.cata (Loc.add_loc info) info loc in @@ -243,19 +243,19 @@ let rec find_pattern nt xl = function | [], NonTerminal x' :: l' -> (out_nt nt,x',List.rev xl),l' | _, Break s :: _ | Break s :: _, _ -> - error ("A break occurs on one side of \"..\" but not on the other side.") + user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side.")) | _, Terminal s :: _ | Terminal s :: _, _ -> user_err ~hdr:"Metasyntax.find_pattern" (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") | _, [] -> - error msg_expected_form_of_recursive_notation + user_err Pp.(str msg_expected_form_of_recursive_notation) | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right") let rec interp_list_parser hd = function | [] -> [], List.rev hd | NonTerminal id :: tl when Id.equal id ldots_var -> - if List.is_empty hd then error msg_expected_form_of_recursive_notation; + if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation); let hd = List.rev hd in let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in let xyl,tl'' = interp_list_parser [] tl' in @@ -286,7 +286,7 @@ let quote_notation_token x = let rec raw_analyze_notation_tokens = function | [] -> [] | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl - | String "_" :: _ -> error "_ must be quoted." + | String "_" :: _ -> user_err Pp.(str "_ must be quoted.") | String x :: sl when CLexer.is_ident x -> NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> @@ -487,7 +487,7 @@ let make_hunks etyps symbols from = (* Build default printing rules from explicit format *) -let error_format () = error "The format does not match the notation." +let error_format () = user_err Pp.(str "The format does not match the notation.") let rec split_format_at_ldots hd = function | UnpTerminal s :: fmt when String.equal s (Id.to_string ldots_var) -> List.rev hd, fmt @@ -500,7 +500,7 @@ and check_no_ldots_in_box = function | UnpBox (_,fmt) -> (try let _ = split_format_at_ldots [] fmt in - error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.") + user_err Pp.(str ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.")) with Exit -> ()) | _ -> () @@ -518,7 +518,7 @@ let read_recursive_format sl fmt = let rec get_tail = function | a :: sepfmt, b :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *) | [], tail -> skip_var_in_recursive_format tail - | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"." in + | _ -> user_err Pp.(str "The format is not the same on the right and left hand side of the special token \"..\".") in let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) @@ -652,7 +652,7 @@ let make_production etyps symbols = distribute [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll | _ -> - error "Components of recursive patterns in notation must be terms or binders.") + user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.")) symbols [[]] in List.map define_keywords prod @@ -811,7 +811,7 @@ let interp_modifiers modl = let open NotationMods in interp { acc with level = Some n; } l | SetAssoc a :: l -> - if not (Option.is_empty acc.assoc) then error "An associativity is given more than once."; + if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once."); interp { acc with assoc = Some a; } l | SetOnlyParsing :: l -> interp { acc with only_parsing = true; } l @@ -820,7 +820,7 @@ let interp_modifiers modl = let open NotationMods in | SetCompatVersion v :: l -> interp { acc with compat = Some v; } l | SetFormat ("text",s) :: l -> - if not (Option.is_empty acc.format) then error "A format is given more than once."; + if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once."); interp { acc with format = Some s; } l | SetFormat (k,(_,s)) :: l -> interp { acc with extra = (k,s)::acc.extra; } l @@ -829,7 +829,7 @@ let interp_modifiers modl = let open NotationMods in let check_infix_modifiers modifiers = let t = (interp_modifiers modifiers).NotationMods.etyps in if not (List.is_empty t) then - error "Explicit entry level or type unexpected in infix notation." + user_err Pp.(str "Explicit entry level or type unexpected in infix notation.") let check_useless_entry_types recvars mainvars etyps = let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in @@ -901,7 +901,7 @@ let internalization_type_of_entry_type = function | ETBigint | ETReference -> NtnInternTypeConstr | ETBinder _ -> NtnInternTypeBinder | ETName -> NtnInternTypeIdent - | ETPattern | ETOther _ -> error "Not supported." + | ETPattern | ETOther _ -> user_err Pp.(str "Not supported.") | ETBinderList _ | ETConstrList _ -> assert false let set_internalization_type typs = @@ -917,7 +917,7 @@ let make_interpretation_type isrec isonlybinding = function | NtnInternTypeConstr | NtnInternTypeIdent -> if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr | NtnInternTypeBinder when isrec -> NtnTypeBinderList - | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders." + | NtnInternTypeBinder -> user_err Pp.(str "Type binder is only for use in recursive notations for binders.") let make_interpretation_vars recvars allvars = let eq_subscope (sc1, l1) (sc2, l2) = @@ -938,9 +938,9 @@ let make_interpretation_vars recvars allvars = let check_rule_productivity l = if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then - error "A notation must include at least one symbol."; + user_err Pp.(str "A notation must include at least one symbol."); if (match l with SProdList _ :: _ -> true | _ -> false) then - error "A recursive notation must start with at least one symbol." + user_err Pp.(str "A recursive notation must start with at least one symbol.") let warn_notation_bound_to_variable = CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing" @@ -980,7 +980,7 @@ let find_precedence lev etyps symbols = | Some (NonTerminal x) -> (try match List.assoc x etyps with | ETConstr _ -> - error "The level of the leftmost non-terminal cannot be changed." + user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") | ETName | ETBigint | ETReference -> begin match lev with | None -> @@ -988,31 +988,31 @@ let find_precedence lev etyps symbols = | Some 0 -> ([],0) | _ -> - error "A notation starting with an atomic expression must be at level 0." + user_err Pp.(str "A notation starting with an atomic expression must be at level 0.") end | ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *) if Option.is_empty lev then - error "Need an explicit level." + user_err Pp.(str "Need an explicit level.") else [],Option.get lev | ETConstrList _ | ETBinderList _ -> assert false (* internally used in grammar only *) with Not_found -> if Option.is_empty lev then - error "A left-recursive notation must have an explicit level." + user_err Pp.(str "A left-recursive notation must have an explicit level.") else [],Option.get lev) | Some (Terminal _) when last_is_terminal () -> if Option.is_empty lev then ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) else [],Option.get lev | Some _ -> - if Option.is_empty lev then error "Cannot determine the level."; + if Option.is_empty lev then user_err Pp.(str "Cannot determine the level."); [],Option.get lev let check_curly_brackets_notation_exists () = try let _ = Notation.level_of_notation "{ _ }" in () with Not_found -> - error "Notations involving patterns of the form \"{ _ }\" are treated \n\ -specially and require that the notation \"{ _ }\" is already reserved." + user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\ +specially and require that the notation \"{ _ }\" is already reserved.") (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) let remove_curly_brackets l = @@ -1081,7 +1081,7 @@ let compute_syntax_data df modifiers = let mods = interp_modifiers modifiers in let onlyprint = mods.only_printing in let onlyparse = mods.only_parsing in - if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'."; + if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); let assoc = Option.append mods.assoc (Some NonA) in let toks = split_notation_string df in let recvars,mainvars,symbols = analyze_notation_tokens toks in @@ -1385,7 +1385,7 @@ let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); with NoSyntaxRule -> - error "Parsing rule for this notation has to be previously declared."); + user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc (* Main entry point *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 64c1560309..be58c67a9e 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 diff --git a/vernac/record.ml b/vernac/record.ml index 10207d0e04..5accc8e379 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -561,7 +561,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id in let isnot_class = match kind with Class false -> false | _ -> true in if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then - error "Priorities only allowed for type class substructures"; + user_err Pp.(str "Priorities only allowed for type class substructures"); (* Now, younger decl in params and fields is on top *) let (pl, ctx), arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a08c79c400..6c1d64cfe9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -139,7 +139,7 @@ let make_cases s = let show_match id = let patterns = try make_cases_aux (Nametab.global id) - with Not_found -> error "Unknown inductive type." + with Not_found -> user_err Pp.(str "Unknown inductive type.") in let pr_branch l = str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" @@ -305,7 +305,7 @@ let print_strategy r = let key = match r with | VarRef id -> VarKey id | ConstRef cst -> ConstKey cst - | IndRef _ | ConstructRef _ -> error "The reference is not unfoldable" + | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable") in let lvl = get_strategy oracle key in Feedback.msg_notice (pr_strategy (r, lvl)) @@ -451,8 +451,8 @@ let start_proof_and_print k l hook = concl (Tacticals.New.tclCOMPLETE tac) in Evd.set_universe_context sigma ctx, EConstr.of_constr c with Logic_monad.TacticFailure e when Logic.catchable_exception e -> - error "The statement obligations could not be resolved \ - automatically, write a statement definition first." + user_err Pp.(str "The statement obligations could not be resolved \ + automatically, write a statement definition first.") in Some hook else None in @@ -551,9 +551,9 @@ let vernac_inductive poly lo finite indl = indl; match indl with | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] -> - CErrors.error "The Record keyword is for types defined using the syntax { ... }." + user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.") | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> - CErrors.error "The Variant keyword does not support syntax { ... }." + user_err Pp.(str "The Variant keyword does not support syntax { ... }.") | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> vernac_record (match b with Class _ -> Class false | _ -> b) poly finite id bl c oc fs @@ -564,16 +564,16 @@ let vernac_inductive poly lo finite indl = (((coe', AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) poly finite id bl c None [f] | [ ( _ , _, _, Class _, Constructors _), [] ] -> - CErrors.error "Inductive classes not supported" + user_err Pp.(str "Inductive classes not supported") | [ ( id , bl , c , Class _, _), _ :: _ ] -> - CErrors.error "where clause not supported for classes" + user_err Pp.(str "where clause not supported for classes") | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> - CErrors.error "where clause not supported for (co)inductive records" + user_err Pp.(str "where clause not supported for (co)inductive records") | _ -> let unpack = function | ( (false, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn | ( (true,_),_,_,_,Constructors _),_ -> - CErrors.error "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead." - | _ -> CErrors.error "Cannot handle mutually (co)inductive records." + user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.") + | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in do_mutual_inductive indl poly lo finite @@ -631,11 +631,11 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then - error "Modules and Module Types are not allowed inside sections."; + user_err Pp.(str "Modules and Module Types are not allowed inside sections."); let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument." + user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast @@ -649,7 +649,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then - error "Modules and Module Types are not allowed inside sections."; + user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mexpr_ast_l with | [] -> check_no_pending_proofs (); @@ -674,7 +674,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." + user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast @@ -694,7 +694,7 @@ let vernac_end_module export (loc,id as lid) = let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then - error "Modules and Module Types are not allowed inside sections."; + user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mty_ast_l with | [] -> @@ -722,7 +722,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." + user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_module_ast @@ -846,7 +846,7 @@ let vernac_set_end_tac tac = let env = Genintern.empty_glob_sign (Global.env ()) in let _, tac = Genintern.generic_intern env tac in if not (refining ()) then - error "Unknown command of the non proof-editing mode."; + user_err Pp.(str "Unknown command of the non proof-editing mode."); set_end_tac tac (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) @@ -903,7 +903,7 @@ let vernac_chdir = function (* Cd is typically used to control the output directory of extraction. A failed Cd could lead to overwriting .ml files so we make it an error. *) - CErrors.error ("Cd failed: " ^ err) + user_err Pp.(str ("Cd failed: " ^ err)) end; if_verbose Feedback.msg_info (str (Sys.getcwd())) @@ -972,7 +972,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags let never_unfold_flag = List.mem `ReductionNeverUnfold flags in let err_incompat x y = - error ("Options \""^x^"\" and \""^y^"\" are incompatible.") in + user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in if assert_flag && rename_flag then err_incompat "assert" "rename"; @@ -1018,7 +1018,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags | { name = Anonymous; notation_scope = Some _ } :: args -> check_extra_args args | _ -> - error "Extra notation scopes can be set on anonymous and explicit arguments only." + user_err Pp.(str "Extra notation scopes can be set on anonymous and explicit arguments only.") in let args, scopes = @@ -1032,12 +1032,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags in if Option.cata (fun n -> n > num_args) false nargs_for_red then - error "The \"/\" modifier should be put before any extra scope."; + user_err Pp.(str "The \"/\" modifier should be put before any extra scope."); let scopes_specified = List.exists Option.has_some scopes in if scopes_specified && clear_scopes_flag then - error "The \"clear scopes\" flag is incompatible with scope annotations."; + user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations."); let names = List.map (fun { name } -> name) args in let names = names :: List.map (List.map fst) more_implicits in @@ -1062,7 +1062,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags | name1 :: names1, name2 :: names2 -> if Name.equal name1 name2 then name1 :: names_union names1 names2 - else error "Argument lists should agree on the names they provide." + else user_err Pp.(str "Argument lists should agree on the names they provide.") in let names = List.fold_left names_union [] names in @@ -1143,10 +1143,10 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags let implicits_specified = match implicits with [[]] -> false | _ -> true in if implicits_specified && clear_implicits_flag then - error "The \"clear implicits\" flag is incompatible with implicit annotations"; + user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); if implicits_specified && default_implicits_flag then - error "The \"default implicits\" flag is incompatible with implicit annotations"; + user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); let rargs = Util.List.map_filter (function (n, true) -> Some n | _ -> None) @@ -1452,8 +1452,8 @@ let vernac_set_strategy locality l = match smart_global r with | ConstRef sp -> EvalConstRef sp | VarRef id -> EvalVarRef id - | _ -> error - "cannot set an inductive type or a constructor as transparent" in + | _ -> user_err Pp.(str + "cannot set an inductive type or a constructor as transparent") in let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in Redexpr.set_strategy local l @@ -1463,8 +1463,8 @@ let vernac_set_opacity locality (v,l) = match smart_global r with | ConstRef sp -> EvalConstRef sp | VarRef id -> EvalVarRef id - | _ -> error - "cannot set an inductive type or a constructor as transparent" in + | _ -> user_err Pp.(str + "cannot set an inductive type or a constructor as transparent") in let l = List.map glob_ref l in Redexpr.set_strategy local [v,l] @@ -1764,10 +1764,10 @@ let vernac_locate = let open Feedback in function let vernac_register id r = if Pfedit.refining () then - error "Cannot register a primitive while in proof editing mode."; + user_err Pp.(str "Cannot register a primitive while in proof editing mode."); let t = (Constrintern.global_reference (snd id)) in if not (isConst t) then - error "Register inline: a constant is expected"; + user_err Pp.(str "Register inline: a constant is expected"); let kn = destConst t in match r with | RegisterInline -> Global.register_inline (Univ.out_punivs kn) @@ -1780,7 +1780,7 @@ let vernac_focus gln = match gln with | None -> Proof.focus focus_command_cond () 1 p | Some 0 -> - CErrors.error "Invalid goal number: 0. Goal numbering starts with 1." + user_err Pp.(str "Invalid goal number: 0. Goal numbering starts with 1.") | Some n -> Proof.focus focus_command_cond () n p) @@ -1795,7 +1795,7 @@ let vernac_unfocused () = if Proof.unfocused p then Feedback.msg_notice (str"The proof is indeed fully unfocused.") else - error "The proof is not fully unfocused." + user_err Pp.(str "The proof is not fully unfocused.") (* BeginSubproof / EndSubproof. @@ -2081,7 +2081,7 @@ let check_vernac_supports_locality c l = | VernacDeclareReduction _ | VernacExtend _ | VernacInductive _) -> () - | Some _, _ -> CErrors.error "This command does not support Locality" + | Some _, _ -> user_err Pp.(str "This command does not support Locality") (* Vernaculars that take a polymorphism flag *) let check_vernac_supports_polymorphism c p = @@ -2095,7 +2095,7 @@ let check_vernac_supports_polymorphism c p = | VernacInstance _ | VernacDeclareInstances _ | VernacHints _ | VernacContext _ | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> () - | Some _, _ -> CErrors.error "This command does not support Polymorphism" + | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism") let enforce_polymorphism = function | None -> Flags.is_universe_polymorphism () @@ -2172,13 +2172,13 @@ let interp ?(verbosely=true) ?proof (loc,c) = | VernacStm _ -> assert false (* Done by Stm *) | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c - | VernacProgram _ -> CErrors.error "Program mode specified twice" + | VernacProgram _ -> user_err Pp.(str "Program mode specified twice") | VernacLocal (b, c) when Option.is_empty locality -> aux ~locality:b ?polymorphism isprogcmd c | VernacPolymorphic (b, c) when polymorphism = None -> aux ?locality ~polymorphism:b isprogcmd c - | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice" - | VernacLocal _ -> CErrors.error "Locality specified twice" + | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice") + | VernacLocal _ -> user_err Pp.(str "Locality specified twice") | VernacFail v -> with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> |