aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml40
-rw-r--r--toplevel/classes.ml3
-rw-r--r--toplevel/coqinit.ml2
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--toplevel/metasyntax.ml14
-rw-r--r--toplevel/metasyntax.mli2
-rw-r--r--toplevel/mltop.ml2
-rw-r--r--toplevel/obligations.ml43
-rw-r--r--toplevel/search.ml27
-rw-r--r--toplevel/usage.ml7
-rw-r--r--toplevel/vernacentries.ml10
11 files changed, 102 insertions, 50 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 7a89b9f54..e99b609b6 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -354,7 +354,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
)))
)
in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
let u,v = destruct_ind type_of_pq
in let lb_type_of_p =
@@ -384,7 +384,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
Tacticals.New.tclTHENLIST [
Proofview.tclEFFECTS eff;
Equality.replace p q ; apply app ; Auto.default_auto]
- end
+ end }
(* used in the bool -> leib side *)
let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
@@ -416,7 +416,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let rec aux l1 l2 =
match (l1,l2) with
| (t1::q1,t2::q2) ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
if eq_constr t1 t2 then aux q1 q2
else (
@@ -457,7 +457,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
aux q1 q2 ]
)
)
- end
+ end }
| ([],[]) -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.")
in
@@ -564,7 +564,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
avoid := fresh::(!avoid); fresh
end gl
in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -587,18 +587,18 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Tacticals.New.tclREPEAT (
Tacticals.New.tclTHENLIST [
Simple.apply_in freshz (andb_prop());
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let fresht = fresh_id (Id.of_string "Z") gl in
(destruct_on_as (mkVar freshz)
[[dl,IntroNaming (IntroIdentifier fresht);
dl,IntroNaming (IntroIdentifier freshz)]])
- end
+ end }
]);
(*
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
- Proofview.Goal.nf_enter begin fun gls ->
+ Proofview.Goal.nf_enter { enter = begin fun gls ->
let gl = Proofview.Goal.concl gls in
match (kind_of_term gl) with
| App (c,ca) -> (
@@ -617,10 +617,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
| _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
)
| _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
- end
+ end }
]
- end
+ end }
let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
@@ -707,7 +707,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
avoid := fresh::(!avoid); fresh
end gl
in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -730,7 +730,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
Tacticals.New.tclTHENLIST [apply (andb_true_intro());
simplest_split ;Auto.default_auto ]
);
- Proofview.Goal.nf_enter begin fun gls ->
+ Proofview.Goal.nf_enter { enter = begin fun gls ->
let gl = Proofview.Goal.concl gls in
(* assume the goal to be eq (eq_type ...) = true *)
match (kind_of_term gl) with
@@ -746,9 +746,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
)
| _ ->
Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
- end
+ end }
]
- end
+ end }
let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
@@ -854,7 +854,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
avoid := fresh::(!avoid); fresh
end gl
in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -885,7 +885,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
)
(Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto);
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let freshH2 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
(* left *)
@@ -897,7 +897,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
;
(*right *)
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let freshH3 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENLIST [
simplest_right ;
@@ -919,11 +919,11 @@ let compute_dec_tact ind lnamesparrec nparrec =
true;
Equality.discr_tac false None
]
- end
+ end }
]
- end
+ end }
]
- end
+ end }
let make_eq_decidability mode mind =
let mib = Global.lookup_mind mind in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index c354c7d32..0a10cfdc3 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -20,6 +20,7 @@ open Libnames
open Globnames
open Constrintern
open Constrexpr
+open Sigma.Notations
(*i*)
open Decl_kinds
@@ -322,7 +323,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
if not (Option.is_empty term) then
let init_refine =
Tacticals.New.tclTHENLIST [
- Proofview.Refine.refine (fun evm -> evm, Option.get term);
+ Proofview.Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
Proofview.Unsafe.tclNEWGOALS gls;
Tactics.New.reduce_after_refine;
]
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index eca344b27..e089b7ecc 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -125,7 +125,7 @@ let init_ocaml_path () =
Mltop.add_ml_dir (Envars.coqlib ());
List.iter add_subdir
[ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
- [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
+ [ "engine" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
[ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ];
[ "grammar" ]; [ "ide" ] ]
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 72966a4ad..4852a6d33 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -480,7 +480,7 @@ let parse_args arglist =
|"-compile-verbose" -> add_compile true (next ())
|"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
|"-feedback-glob" -> Dumpglob.feedback_glob ()
- |"-exclude-dir" -> exclude_search_in_dirname (next ())
+ |"-exclude-dir" -> System.exclude_directory (next ())
|"-init-file" -> set_rcfile (next ())
|"-inputstate"|"-is" -> set_inputstate (next ())
|"-load-ml-object" -> Mltop.dir_ml_load (next ())
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7616bfff6..7714cc810 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -49,7 +49,7 @@ let interp_prod_item lev = function
| TacTerm s -> GramTerminal s
| TacNonTerm (loc, nt, po) ->
let sep = match po with Some (_,sep) -> sep | _ -> "" in
- let (etyp, e) = interp_entry_name true (Some lev) nt sep in
+ let EntryName (etyp, e) = interp_entry_name true (TgTactic lev) nt sep in
GramNonTerminal (loc, etyp, e, Option.map fst po)
let make_terminal_status = function
@@ -58,7 +58,7 @@ let make_terminal_status = function
let rec make_tags = function
| GramTerminal s :: l -> make_tags l
- | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l
+ | GramNonTerminal (loc, etyp, _, po) :: l -> Genarg.unquote etyp :: make_tags l
| [] -> []
let make_fresh_key =
@@ -160,20 +160,22 @@ type atomic_entry = string * Genarg.glob_generic_argument list option
type ml_tactic_grammar_obj = {
mltacobj_name : Tacexpr.ml_tactic_name;
(** ML-side unique name *)
- mltacobj_prod : grammar_prod_item list list;
+ mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list;
(** Grammar rules generating the ML tactic. *)
}
(** ML tactic notations whose use can be restricted to an identifier are added
as true Ltac entries. *)
let extend_atomic_tactic name entries =
- let add_atomic (id, args) = match args with
+ let add_atomic i (id, args) = match args with
| None -> ()
| Some args ->
- let body = Tacexpr.TacML (Loc.ghost, name, args) in
+ let open Tacexpr in
+ let entry = { mltac_name = name; mltac_index = i } in
+ let body = TacML (Loc.ghost, entry, args) in
Tacenv.register_ltac false false (Names.Id.of_string id) body
in
- List.iter add_atomic entries
+ List.iteri add_atomic entries
let cache_ml_tactic_notation (_, obj) =
extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index f22839f48..f7049999e 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -24,7 +24,7 @@ val add_tactic_notation :
type atomic_entry = string * Genarg.glob_generic_argument list option
val add_ml_tactic_notation : ml_tactic_name ->
- Egramml.grammar_prod_item list list -> atomic_entry list -> unit
+ Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> atomic_entry list -> unit
(** Adding a (constr) notation in the environment*)
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index a7fb7a58f..fa5ed7bbd 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -155,7 +155,7 @@ let add_ml_dir s =
| WithoutTop when has_dynlink -> keep_copy_mlpath s
| _ -> ()
-(* For Rec Add ML Path *)
+(* For Rec Add ML Path (-R) *)
let add_rec_ml_dir unix_path =
List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index e488f84f8..0e2de74aa 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -592,14 +592,16 @@ let declare_mutual_definition l =
List.iter progmap_remove l; kn
let shrink_body c =
- let ctx, b = decompose_lam c in
+ let ctx, b = decompose_lam_assum c in
let b', n, args =
- List.fold_left (fun (b, i, args) (n,t) ->
+ List.fold_left (fun (b, i, args) (n, u, t) ->
if noccurn 1 b then
subst1 mkProp b, succ i, args
- else mkLambda (n,t,b), succ i, mkRel i :: args)
+ else
+ let args = if Option.is_empty u then mkRel i :: args else args in
+ mkLambda_or_LetIn (n, u, t) b, succ i, args)
(b, 1, []) ctx
- in List.map (fun (c,t) -> (c,None,t)) ctx, b', Array.of_list args
+ in ctx, b', Array.of_list args
let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
@@ -803,6 +805,36 @@ let solve_by_tac name evi t poly ctx =
Inductiveops.control_only_guard (Global.env ()) (fst body);
(fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
+let obligation_terminator name num guard hook pf =
+ let open Proof_global in
+ let term = Lemmas.universe_proof_terminator guard hook in
+ match pf with
+ | Admitted _ -> apply_terminator term pf
+ | Proved (opq, id, proof) ->
+ if not !shrink_obligations then apply_terminator term pf
+ else
+ let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
+ let env = Global.env () in
+ let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
+ let ty = entry.Entries.const_entry_type in
+ let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
+ assert(Safe_typing.empty_private_constants = eff);
+ assert(Univ.ContextSet.is_empty cstr);
+ Inductiveops.control_only_guard (Global.env ()) body;
+ (** Declare the obligation ourselves and drop the hook *)
+ let prg = get_info (ProgMap.find name !from_prg) in
+ let prg = { prg with prg_ctx = uctx } in
+ let obls, rem = prg.prg_obligations in
+ let obl = obls.(num) in
+ let ctx = Evd.evar_context_universe_context uctx in
+ let (_, obl) = declare_obligation prg obl body ty ctx in
+ let obls = Array.copy obls in
+ let _ = obls.(num) <- obl in
+ try ignore (update_obls prg obls (pred rem))
+ with e when Errors.noncritical e ->
+ let e = Errors.push e in
+ pperror (Errors.iprint (Cerrors.process_vernac_interp_error e))
+
let obligation_hook prg obl num auto ctx' _ gr =
let obls, rem = prg.prg_obligations in
let cst = match gr with ConstRef cst -> cst | _ -> assert false in
@@ -852,8 +884,9 @@ let rec solve_obligation prg num tac =
let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
let evd = Evd.from_ctx prg.prg_ctx in
let auto n tac oblset = auto_solve_obligations n ~oblset tac in
+ let terminator guard hook = Proof_global.make_terminator (obligation_terminator prg.prg_name num guard hook) in
let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
- let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type hook in
+ let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type ~terminator hook in
let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in
let _ = Pfedit.by (snd (get_default_tactic ())) in
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 9e67eef00..9c32bddad 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -18,10 +18,28 @@ open Printer
open Libnames
open Globnames
open Nametab
+open Goptions
type filter_function = global_reference -> env -> constr -> bool
type display_function = global_reference -> env -> constr -> unit
+(* This option restricts the output of [SearchPattern ...],
+[SearchAbout ...], etc. to the names of the symbols matching the
+query, separated by a newline. This type of output is useful for
+editors (like emacs), to generate a list of completion candidates
+without having to parse thorugh the types of all symbols. *)
+
+let search_output_name_only = ref false
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "output-name-only search";
+ optkey = ["Search";"Output";"Name";"Only"];
+ optread = (fun () -> !search_output_name_only);
+ optwrite = (:=) search_output_name_only }
+
type glob_search_about_item =
| GlobSearchSubPattern of constr_pattern
| GlobSearchString of string
@@ -98,11 +116,14 @@ let generic_search glnumopt fn =
iter_declarations fn
(** Standard display *)
-
let plain_display accu ref env c =
- let pc = pr_lconstr_env env Evd.empty c in
let pr = pr_global ref in
- accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu
+ if !search_output_name_only then
+ accu := pr :: !accu
+ else begin
+ let pc = pr_lconstr_env env Evd.empty c in
+ accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu
+ end
let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 472503ced..292136406 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -114,12 +114,7 @@ let print_config () =
if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
Printf.printf "COQLIB=%s/\n" (Envars.coqlib ());
Printf.printf "DOCDIR=%s/\n" (Envars.docdir ());
- Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep;
- Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc;
- Printf.printf "OCAMLOPT=%s\n" Coq_config.ocamlopt;
- Printf.printf "OCAMLDOC=%s\n" Coq_config.ocamldoc;
- Printf.printf "CAMLBIN=%s/\n" (Envars.camlbin ());
- Printf.printf "CAMLLIB=%s/\n" (Envars.camllib ());
+ Printf.printf "OCAMLFIND=%s\n" (Envars.ocamlfind ());
Printf.printf "CAMLP4=%s\n" Coq_config.camlp4;
Printf.printf "CAMLP4O=%s\n" Coq_config.camlp4o;
Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ());
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 31bfc004a..bf090384d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -347,7 +347,7 @@ let dump_universes_gen g s =
end
in
try
- Univ.dump_universes output_constraint g;
+ UGraph.dump_universes output_constraint g;
close ();
msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
with reraise ->
@@ -357,7 +357,7 @@ let dump_universes_gen g s =
let dump_universes sorted s =
let g = Global.universes () in
- let g = if sorted then Univ.sort_universes g else g in
+ let g = if sorted then UGraph.sort_universes g else g in
dump_universes_gen g s
(*********************)
@@ -1559,7 +1559,7 @@ let vernac_global_check c =
let sigma = Evd.from_env env in
let c,ctx = interp_constr env sigma c in
let senv = Global.safe_env() in
- let cstrs = snd (Evd.evar_universe_context_set Univ.UContext.empty ctx) in
+ let cstrs = snd (UState.context_set ctx) in
let senv = Safe_typing.add_constraints cstrs senv in
let j = Safe_typing.typing senv c in
let env = Safe_typing.env_of_safe_env senv in
@@ -1625,12 +1625,12 @@ let vernac_print = function
| PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
| PrintUniverses (b, None) ->
let univ = Global.universes () in
- let univ = if b then Univ.sort_universes univ else univ in
+ let univ = if b then UGraph.sort_universes univ else univ in
let pr_remaining =
if Global.is_joined_environment () then mt ()
else str"There may remain asynchronous universe constraints"
in
- msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
+ msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
| PrintUniverses (b, Some s) -> dump_universes b s
| PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
| PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 06:44:41 +0000