diff options
| author | Enrico Tassi | 2015-03-09 18:44:33 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-03-11 11:42:10 +0100 |
| commit | f36f1d07ee0b9b40d54b9fece942b00e8e5e5d50 (patch) | |
| tree | 4b3d9cf2a0ed1ef4faa1d6bfccaaf0ca878a942d | |
| parent | e4ad47fed594d6865f5bd29a159976cb072f0fae (diff) | |
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
129 files changed, 288 insertions, 117 deletions
@@ -154,6 +154,13 @@ Tactics refine, use "refine c;shelve_unifiable". This can still cause incompatibilities in rare occasions. * New "give_up" tactic to skip over a goal without admitting it. +- The admit tactic has been removed, "give_up" should be used instead. + To compile code containing "admit" the following solutions can be adopted: + * Add Ltac definition "Ltac admit := give_up." and terminate each + incomplete proof with "Admitted". + * Add an "Axiom" for each admitted subproof. + * Add a single "Axiom proof_admitted : False." and the Ltac definition + "Ltac admit := case proof_admitted.". - Matching using "lazymatch" was fundamentally modified. It now behaves like "match" (immediate execution of the matching branch) but without the backtracking mechanism in case of failure. @@ -322,7 +329,7 @@ Interfaces errors are reported in the bottom right window. The number of workers taking care of processing proofs can be selected with -async-proofs-j. - CoqIDE highlights in yellow "unsafe" commands such as axiom - declarations, and tactics like "admit". + declarations, and tactics like "give_up". - CoqIDE supports Proof General like key bindings; to activate the PG mode go to Edit -> Preferences -> Editor. For the documentation see Help -> Help for PG mode. @@ -541,7 +548,7 @@ Vernacular commands - New command "Add/Remove Search Blacklist <substring> ...": a Search or SearchAbout or similar query will never mention lemmas whose qualified names contain any of the declared substrings. - The default blacklisted substrings are "_admitted" "_subproof" "Private_". + The default blacklisted substrings are "_subproof" "Private_". - When the output file of "Print Universes" ends in ".dot" or ".gv", the universe graph is printed in the DOT language, and can be processed by Graphviz tools. diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 5a66910722..589933578a 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1465,7 +1465,7 @@ You can use the {\tt Clear} command. \Question{How can use a proof which is not finished?} You can use the {\tt Admitted} command to state your current proof as an axiom. -You can use the {\tt admit} tactic to omit a portion of a proof. +You can use the {\tt give\_up} tactic to omit a portion of a proof. \Question{How can I state a conjecture?} diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 32f94abf7a..556a2dab58 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -432,7 +432,7 @@ the search results via the command {\tt Add Search Blacklist "substring1"}. A lemma whose fully-qualified name contains any of the declared substrings will be removed from the search results. -The default blacklisted substrings are {\tt "\_admitted" +The default blacklisted substrings are {\tt "\_subproof" "Private\_"}. The command {\tt Remove Search Blacklist ...} allows expunging this blacklist. diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 52f32d0c7d..2eebac18e6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1439,18 +1439,6 @@ a hypothesis or in the body or the type of a local definition. \end{Variants} -\subsection{\tt admit} -\tacindex{admit} -\label{admit} - -The {\tt admit} tactic ``solves'' the current subgoal by an -axiom. This typically allows temporarily skipping a subgoal so as to -progress further in the rest of the proof. To know if some proof still -relies on unproved subgoals, one can use the command {\tt Print -Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals -have names of the form {\ident}\texttt{\_admitted} possibly followed -by a number. - \subsection{\tt absurd \term} \tacindex{absurd} \label{absurd} diff --git a/interp/coqlib.ml b/interp/coqlib.ml index e722615a9b..02504c9202 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -349,7 +349,6 @@ let build_coq_inversion_eq_true_data () = (* The False proposition *) let coq_False = lazy_init_constant ["Logic"] "False" -let coq_proof_admitted = lazy_init_constant ["Logic"] "proof_admitted" (* The True proposition and its unique proof *) let coq_True = lazy_init_constant ["Logic"] "True" @@ -371,7 +370,6 @@ let build_coq_True () = Lazy.force coq_True let build_coq_I () = Lazy.force coq_I let build_coq_False () = Lazy.force coq_False -let build_coq_proof_admitted () = Lazy.force coq_proof_admitted let build_coq_not () = Lazy.force coq_not let build_coq_and () = Lazy.force coq_and let build_coq_conj () = Lazy.force coq_conj diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 986a4385c1..41204a715b 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -160,7 +160,6 @@ val build_coq_sumbool : constr delayed (** Connectives The False proposition *) val build_coq_False : constr delayed -val build_coq_proof_admitted : constr delayed (** The True proposition and its unique proof *) val build_coq_True : constr delayed diff --git a/library/library.ml b/library/library.ml index 95b817d0a1..7513cf8387 100644 --- a/library/library.ml +++ b/library/library.ml @@ -696,7 +696,7 @@ let save_library_to ?todo dir f otab = f ^ "o", Future.UUIDSet.empty | Some (l,_) -> f ^ "io", - List.fold_left (fun e r -> Future.UUIDSet.add r.Stateid.uuid e) + List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in let cenv, seg, ast = Declaremods.end_library ~except dir in let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in @@ -705,14 +705,17 @@ let save_library_to ?todo dir f otab = | None -> None, None, None | Some (tasks, rcbackup) -> let tasks = - List.map Stateid.(fun r -> - { r with uuid = Future.UUIDMap.find r.uuid f2t_map }) tasks in + List.map Stateid.(fun (r,b) -> + try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b + with Not_found -> assert b; { r with uuid = -1 }, b) + tasks in Some (tasks,rcbackup), Some (univ_table,Univ.ContextSet.empty,false), Some disch_table in let except = Future.UUIDSet.fold (fun uuid acc -> - Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc) + try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc + with Not_found -> acc) except Int.Set.empty in let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in Array.iteri (fun i x -> diff --git a/library/library.mli b/library/library.mli index 77d78207da..75b256258f 100644 --- a/library/library.mli +++ b/library/library.mli @@ -44,7 +44,7 @@ val start_library : string -> DirPath.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) val save_library_to : - ?todo:((Future.UUID.t,'document) Stateid.request list * 'counters) -> + ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index a77b552e01..c232ae31ad 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -49,7 +49,7 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted -> Errors.error"Admitted isn't supported in Derive." + | Admitted _ -> Errors.error"Admitted isn't supported in Derive." | Proved (_,Some _,_) -> Errors.error"Cannot save a proof of Derive with an explicit name." | Proved (opaque, None, obj) -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9717292456..2917f52c58 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -74,7 +74,7 @@ type proof_object = { } type proof_ending = - | Admitted + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object @@ -338,8 +338,22 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context -let return_proof () = - let { pid; proof; strength = (_,poly,_) } = cur_pstate () in +let return_proof ?(allow_partial=false) () = + let { pid; proof; strength = (_,poly,_) } = cur_pstate () in + if allow_partial then begin + if Proof.is_done proof then begin + msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++ + str" is complete, no need to end it with Admitted"); + end; + let proofs = Proof.partial_proof proof in + let _,_,_,_, evd = Proof.proof proof in + let eff = Evd.eval_side_effects evd in + (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) + let proofs = List.map (fun c -> c, eff) proofs in + proofs, Evd.evar_universe_context evd + end else let initial_goals = Proof.initial_goals proof in let evd = let error s = @@ -352,10 +366,9 @@ let return_proof () = | Proof.HasShelvedGoals -> error(str"Attempt to save a proof with shelved goals") | Proof.HasGivenUpGoals -> - error(str"Attempt to save a proof with given up goals") + error(strbrk"Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.") | Proof.HasUnresolvedEvar-> - error(str"Attempt to save a proof with existential " ++ - str"variables still non-instantiated") in + error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in let evd = if poly || !Flags.compilation_mode = Flags.BuildVo diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 2700e90123..9d5038a3f9 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -66,7 +66,7 @@ type proof_object = { } type proof_ending = - | Admitted + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object @@ -99,7 +99,9 @@ val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context -val return_proof : unit -> closed_proof_output +(* If allow_partial is set (default no) then an incomplete proof + * is allowed (no error), and a warn is given if the proof is complete. *) +val return_proof : ?allow_partial:bool -> unit -> closed_proof_output val close_future_proof : feedback_id:Stateid.t -> closed_proof_output Future.computation -> closed_proof diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 63c45116a6..6cece32e0a 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -296,13 +296,7 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident = (* Admitted *) -let admit hook () = - let (id,k,typ) = Pfedit.current_proof_statement () in - let ctx = - let evd = fst (Pfedit.get_current_goal_context ()) in - Evd.universe_context evd - in - let e = Pfedit.get_used_variables(), pi2 k, (typ, ctx), None in +let admit (id,k,e) hook () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in let () = match k with | Global, _, _ -> () @@ -334,8 +328,8 @@ let check_exist = let standard_proof_terminator compute_guard hook = let open Proof_global in function - | Admitted -> - admit hook (); + | Admitted (id,k,pe) -> + admit (id,k,pe) hook (); Pp.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff, exports = match opaque with @@ -353,8 +347,8 @@ let standard_proof_terminator compute_guard hook = let universe_proof_terminator compute_guard hook = let open Proof_global in function - | Admitted -> - admit (hook None) (); + | Admitted (id,k,pe) -> + admit (id,k,pe) (hook None) (); Pp.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff, exports = match opaque with @@ -475,7 +469,37 @@ let start_proof_com kind thms hook = let save_proof ?proof = function | Vernacexpr.Admitted -> - Proof_global.get_terminator() Proof_global.Admitted + let pe = + let open Proof_global in + match proof with + | Some ({ id; entries; persistence = k; universes }, _) -> + if List.length entries <> 1 then + error "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"; + let typ = Option.get const_entry_type in + let ctx = Evd.evar_context_universe_context universes in + Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None)) + | None -> + let id, k, typ = Pfedit.current_proof_statement () in + let ctx = + let evd, _ = Pfedit.get_current_goal_context () in + Evd.universe_context evd in + (* This will warn if the proof is complete *) + let pproofs,_ = Proof_global.return_proof ~allow_partial:true () in + let sec_vars = + match Pfedit.get_used_variables(), pproofs with + | Some _ as x, _ -> x + | None, (pproof, _) :: _ -> + let env = Global.env () in + let ids_typ = Environ.global_vars_set env typ in + let ids_def = Environ.global_vars_set env pproof in + Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) + | _ -> None in + Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None)) + in + Proof_global.get_terminator() pe | Vernacexpr.Proved (is_opaque,idopt) -> let (proof_obj,terminator) = match proof with diff --git a/stm/stm.ml b/stm/stm.ml index b38407c045..092f8eed1d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -905,6 +905,7 @@ module rec ProofTask : sig t_exn_info : Stateid.t * Stateid.t; t_start : Stateid.t; t_stop : Stateid.t; + t_drop : bool; t_states : competence; t_assign : Proof_global.closed_proof_output Future.assignement -> unit; t_loc : Loc.t; @@ -916,8 +917,8 @@ module rec ProofTask : sig | States of Stateid.t list type request = - | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * competence - | ReqStates of Stateid.t list + | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence + | ReqStates of Stateid.t list include AsyncTaskQueue.Task with type task := task @@ -925,6 +926,7 @@ module rec ProofTask : sig and type request := request val build_proof_here : + drop_pt:bool -> Stateid.t * Stateid.t -> Loc.t -> Stateid.t -> Proof_global.closed_proof_output Future.computation @@ -940,6 +942,7 @@ end = struct (* {{{ *) t_exn_info : Stateid.t * Stateid.t; t_start : Stateid.t; t_stop : Stateid.t; + t_drop : bool; t_states : competence; t_assign : Proof_global.closed_proof_output Future.assignement -> unit; t_loc : Loc.t; @@ -951,8 +954,8 @@ end = struct (* {{{ *) | States of Stateid.t list type request = - | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * competence - | ReqStates of Stateid.t list + | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence + | ReqStates of Stateid.t list type error = { e_error_at : Stateid.t; @@ -985,12 +988,14 @@ end = struct (* {{{ *) | BuildProof t -> "proof: " ^ t.t_name | States l -> "states: " ^ String.concat "," (List.map Stateid.to_string l) let name_of_request = function - | ReqBuildProof(r,_) -> "proof: " ^ r.Stateid.name + | ReqBuildProof(r,_,_) -> "proof: " ^ r.Stateid.name | ReqStates l -> "states: "^String.concat "," (List.map Stateid.to_string l) let request_of_task age = function | States l -> Some (ReqStates l) - | BuildProof { t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states } -> + | BuildProof { + t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states;t_drop + } -> assert(age = `Fresh); try Some (ReqBuildProof ({ Stateid.exn_info = t_exn_info; @@ -998,7 +1003,7 @@ end = struct (* {{{ *) document = VCS.slice ~start:t_start ~stop:t_stop; loc = t_loc; uuid = t_uuid; - name = t_name }, t_states)) + name = t_name }, t_drop, t_states)) with VCS.Expired -> None let use_response (s : competence AsyncTaskQueue.worker_status) t r = @@ -1032,7 +1037,7 @@ end = struct (* {{{ *) Hooks.(call execution_error start Loc.ghost (strbrk s)); feedback (Feedback.InProgress ~-1) - let build_proof_here (id,valid) loc eop = + let build_proof_here ~drop_pt (id,valid) loc eop = Future.create (State.exn_on id ~valid) (fun () -> let wall_clock1 = Unix.gettimeofday () in if !Flags.batch_mode then Reach.known_state ~cache:`No eop @@ -1040,31 +1045,35 @@ end = struct (* {{{ *) let wall_clock2 = Unix.gettimeofday () in Aux_file.record_in_aux_at loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); - Proof_global.return_proof ()) + let p = Proof_global.return_proof ~allow_partial:drop_pt () in + if drop_pt then Pp.feedback ~state_id:id Feedback.Complete; + p) - let perform_buildp { Stateid.exn_info; stop; document; loc } my_states = + let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states = try VCS.restore document; VCS.print (); let proof, future_proof, time = let wall_clock = Unix.gettimeofday () in - let fp = build_proof_here exn_info loc stop in + let fp = build_proof_here ~drop_pt:drop exn_info loc stop in let proof = Future.force fp in proof, fp, Unix.gettimeofday () -. wall_clock in (* We typecheck the proof with the kernel (in the worker) to spot * the few errors tactics don't catch, like the "fix" tactic building * a bad fixpoint *) let fix_exn = Future.fix_exn_of future_proof in - let checked_proof = Future.chain ~pure:false future_proof (fun p -> - let pobject, _ = - Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in - let terminator = (* The one sent by master is an InvalidKey *) - Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in - vernac_interp stop - ~proof:(pobject, terminator) - { verbose = false; loc; - expr = (VernacEndProof (Proved (Opaque None,None))) }) in - ignore(Future.join checked_proof); + if not drop then begin + let checked_proof = Future.chain ~pure:false future_proof (fun p -> + let pobject, _ = + Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in + let terminator = (* The one sent by master is an InvalidKey *) + Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in + vernac_interp stop + ~proof:(pobject, terminator) + { verbose = false; loc; + expr = (VernacEndProof (Proved (Opaque None,None))) }) in + ignore(Future.join checked_proof); + end; RespBuiltProof(proof,time) with | e when Errors.noncritical e || e = Stack_overflow -> @@ -1115,17 +1124,17 @@ end = struct (* {{{ *) aux [initial] query let perform = function - | ReqBuildProof (bp,states) -> perform_buildp bp states + | ReqBuildProof (bp,drop,states) -> perform_buildp bp drop states | ReqStates sl -> RespStates (perform_states sl) let on_marshal_error s = function | States _ -> msg_error(strbrk("Marshalling error: "^s^". "^ "The system state could not be sent to the master process.")) - | BuildProof { t_exn_info; t_stop; t_assign; t_loc } -> + | BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } -> msg_error(strbrk("Marshalling error: "^s^". "^ "The system state could not be sent to the worker process. "^ "Falling back to local, lazy, evaluation.")); - t_assign(`Comp(build_proof_here t_exn_info t_loc t_stop)); + t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop)); feedback (Feedback.InProgress ~-1) end (* }}} *) @@ -1134,7 +1143,8 @@ end (* }}} *) and Slaves : sig (* (eventually) remote calls *) - val build_proof : loc:Loc.t -> + val build_proof : + loc:Loc.t -> drop_pt:bool -> exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t -> name:string -> future_proof * cancel_switch @@ -1144,7 +1154,7 @@ and Slaves : sig (* initialize the whole machinery (optional) *) val init : unit -> unit - type 'a tasks = ('a,VCS.vcs) Stateid.request list + type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list val dump_snapshot : unit -> Future.UUID.t tasks val check_task : string -> int tasks -> int -> bool val info_tasks : 'a tasks -> (string * float * int) list @@ -1172,7 +1182,7 @@ end = struct (* {{{ *) queue := Some (TaskQueue.create 0) let check_task_aux extra name l i = - let { Stateid.stop; document; loc; name = r_name } = List.nth l i in + let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in msg_info( str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); VCS.restore document; @@ -1183,6 +1193,10 @@ end = struct (* {{{ *) aux stop in try Reach.known_state ~cache:`No stop; + if drop then + let _proof = Proof_global.return_proof ~allow_partial:true () in + `OK_ADMITTED + else begin (* The original terminator, a hook, has not been saved in the .vio*) Proof_global.set_terminator (Lemmas.standard_proof_terminator [] @@ -1195,7 +1209,8 @@ end = struct (* {{{ *) vernac_interp stop ~proof { verbose = false; loc; expr = (VernacEndProof (Proved (Opaque None,None))) }; - Some proof + `OK proof + end with e -> let (e, info) = Errors.push e in (try match Stateid.get info with @@ -1220,13 +1235,19 @@ end = struct (* {{{ *) spc () ++ iprint (e, info)) with e -> msg_error (str"unable to print error message: " ++ - str (Printexc.to_string e))); None + str (Printexc.to_string e))); + if drop then `ERROR_ADMITTED else `ERROR let finish_task name (u,cst,_) d p l i = - let bucket = (List.nth l i).Stateid.uuid in - match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with - | None -> exit 1 - | Some (po,_) -> + let { Stateid.uuid = bucket }, drop = List.nth l i in + let bucket_name = + if bucket < 0 then (assert drop; ", no bucket") + else Printf.sprintf ", bucket %d" bucket in + match check_task_aux bucket_name name l i with + | `ERROR -> exit 1 + | `ERROR_ADMITTED -> u, cst, false + | `OK_ADMITTED -> u, cst, false + | `OK (po,_) -> let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in let con = Nametab.locate_constant @@ -1253,11 +1274,11 @@ end = struct (* {{{ *) let check_task name l i = match check_task_aux "" name l i with - | Some _ -> true - | None -> false + | `OK _ | `OK_ADMITTED -> true + | `ERROR | `ERROR_ADMITTED -> false let info_tasks l = - CList.map_i (fun i { Stateid.loc; name } -> + CList.map_i (fun i ({ Stateid.loc; name }, _) -> let time1 = try float_of_string (Aux_file.get !hints loc "proof_build_time") with Not_found -> 0.0 in @@ -1284,7 +1305,7 @@ end = struct (* {{{ *) BuildProof { t_states = s2 } -> overlap_rel s1 s2 | _ -> 0) - let build_proof ~loc ~exn_info ~start ~stop ~name:pname = + let build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name:pname = let id, valid as t_exn_info = exn_info in let cancel_switch = ref false in if TaskQueue.n_workers (Option.get !queue) = 0 then @@ -1293,19 +1314,19 @@ end = struct (* {{{ *) Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in let task = ProofTask.(BuildProof { - t_exn_info; t_start = start; t_stop = stop; + t_exn_info; t_start = start; t_stop = stop; t_drop = drop_pt; t_assign = assign; t_loc = loc; t_uuid; t_name = pname; t_states = VCS.nodes_in_slice ~start ~stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); f, cancel_switch end else - ProofTask.build_proof_here t_exn_info loc stop, cancel_switch + ProofTask.build_proof_here ~drop_pt t_exn_info loc stop, cancel_switch else let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in feedback (Feedback.InProgress 1); let task = ProofTask.(BuildProof { - t_exn_info; t_start = start; t_stop = stop; t_assign; + t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt; t_loc = loc; t_uuid; t_name = pname; t_states = VCS.nodes_in_slice ~start ~stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); @@ -1316,14 +1337,14 @@ end = struct (* {{{ *) let cancel_worker n = TaskQueue.cancel_worker (Option.get !queue) n (* For external users this name is nicer than request *) - type 'a tasks = ('a,VCS.vcs) Stateid.request list + type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list let dump_snapshot () = let tasks = TaskQueue.snapshot (Option.get !queue) in let reqs = CList.map_filter ProofTask.(fun x -> match request_of_task `Fresh x with - | Some (ReqBuildProof (r, _)) -> Some r + | Some (ReqBuildProof (r, b, _)) -> Some(r, b) | _ -> None) tasks in prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length reqs)); @@ -1656,7 +1677,7 @@ let collect_proof keep cur hd brkind id = else if keep == VtDrop then `Sync (no_name,None,`Aborted) else let rc = collect (Some cur) [] id in - if keep == VtKeep && + if (keep == VtKeep || keep == VtKeepAsAxiom) && (not(State.is_cached id) || !Flags.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -1733,7 +1754,8 @@ let known_state ?(redefine_qed=false) ~cache id = | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function | `ASync (start, pua, nodes, name, delegate) -> (fun () -> - assert(keep == VtKeep); + assert(keep == VtKeep || keep == VtKeepAsAxiom); + let drop_pt = keep == VtKeepAsAxiom in let stop, exn_info, loc = eop, (id, eop), x.loc in prerr_endline ("Asynchronous " ^ Stateid.to_string id); VCS.create_cluster nodes ~qed:id ~start; @@ -1742,7 +1764,8 @@ let known_state ?(redefine_qed=false) ~cache id = | { VCS.kind = `Edit _ }, Some (ofp, cancel) -> assert(redefine_qed = true); let fp, cancel = - Slaves.build_proof ~loc ~exn_info ~start ~stop ~name in + Slaves.build_proof + ~loc ~drop_pt ~exn_info ~start ~stop ~name in Future.replace ofp fp; qed.fproof <- Some (fp, cancel) | { VCS.kind = `Proof _ }, Some _ -> assert false @@ -1750,9 +1773,11 @@ let known_state ?(redefine_qed=false) ~cache id = reach ~cache:`Shallow start; let fp, cancel = if delegate then - Slaves.build_proof ~loc ~exn_info ~start ~stop ~name + Slaves.build_proof + ~loc ~drop_pt ~exn_info ~start ~stop ~name else - ProofTask.build_proof_here exn_info loc stop, ref false + ProofTask.build_proof_here + ~drop_pt exn_info loc stop, ref false in qed.fproof <- Some (fp, cancel); let proof = @@ -1776,11 +1801,16 @@ let known_state ?(redefine_qed=false) ~cache id = let wall_clock = Unix.gettimeofday () in record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork); let proof = - if keep != VtKeep then None - else Some(Proof_global.close_proof - ~keep_body_ucst_sepatate:false - (State.exn_on id ~valid:eop)) in - if proof = None then prerr_endline "NONE!!!!!"; + match keep with + | VtDrop -> None + | VtKeepAsAxiom -> + let ctx = Evd.empty_evar_universe_context in + let fp = Future.from_val ([],ctx) in + qed.fproof <- Some (fp, ref false); None + | VtKeep -> + Some(Proof_global.close_proof + ~keep_body_ucst_sepatate:false + (State.exn_on id ~valid:eop)) in reach view.next; if keep == VtKeepAsAxiom then Option.iter (vernac_interp id) pua; @@ -1862,11 +1892,22 @@ let wait () = Slaves.wait_all_done (); VCS.print () +let rec join_admitted_proofs id = + if Stateid.equal id Stateid.initial then () else + let view = VCS.visit id in + match view.step with + | `Qed ({ keep = VtKeepAsAxiom; fproof = Some (fp,_) },_) -> + ignore(Future.force fp); + join_admitted_proofs view.next + | _ -> join_admitted_proofs view.next + let join () = finish (); wait (); prerr_endline "Joining the environment"; Global.join_safe_environment (); + prerr_endline "Joining Admitted proofs"; + join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); VCS.print (); VCS.print () diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1ffc0519fe..891e2dba51 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -25,13 +25,9 @@ open Misctypes DECLARE PLUGIN "extratactics" (**********************************************************************) -(* admit, replace, discriminate, injection, simplify_eq *) +(* replace, discriminate, injection, simplify_eq *) (* cutrewrite, dependent rewrite *) -TACTIC EXTEND admit - [ "admit" ] -> [ admit_as_an_axiom ] -END - let replace_in_clause_maybe_by (sigma1,c1) c2 cl tac = Tacticals.New.tclWITHHOLES false (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac)) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ad6684e25b..b1559da33f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4411,11 +4411,6 @@ let tclABSTRACT name_op tac = in abstract_subproof s gk tac -let admit_as_an_axiom = - Proofview.tclUNIT () >>= fun () -> (* delay for Coqlib.build_coq_proof_admitted *) - simplest_case (Coqlib.build_coq_proof_admitted ()) <*> - Proofview.mark_as_unsafe - let unify ?(state=full_transparent_state) x y = Proofview.Goal.nf_enter begin fun gl -> try diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6025883fe6..eea4956214 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -393,8 +393,6 @@ val unify : ?state:Names.transparent_state -> constr -> constr -> unit val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic -val admit_as_an_axiom : unit Proofview.tactic - val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> tactic diff --git a/test-suite/_CoqProject b/test-suite/_CoqProject new file mode 100644 index 0000000000..dc121311d0 --- /dev/null +++ b/test-suite/_CoqProject @@ -0,0 +1 @@ +-Q prerequisite TestSuite diff --git a/test-suite/bugs/closed/1704.v b/test-suite/bugs/closed/1704.v index 4b02d5f93b..7d8ba5b8da 100644 --- a/test-suite/bugs/closed/1704.v +++ b/test-suite/bugs/closed/1704.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Import Setoid. Parameter E : nat -> nat -> Prop. diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index 35c69db2fe..85ad41d1cf 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* test with Coq 8.3rc1 *) Require Import Program. diff --git a/test-suite/bugs/closed/2473.v b/test-suite/bugs/closed/2473.v index 4c3025128c..fb676c7e47 100644 --- a/test-suite/bugs/closed/2473.v +++ b/test-suite/bugs/closed/2473.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Import Relations Program Setoid Morphisms. diff --git a/test-suite/bugs/closed/2590.v b/test-suite/bugs/closed/2590.v index e594e96936..4300de16e0 100644 --- a/test-suite/bugs/closed/2590.v +++ b/test-suite/bugs/closed/2590.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Import Relation_Definitions RelationClasses Setoid SetoidClass. Section Bug. diff --git a/test-suite/bugs/closed/2613.v b/test-suite/bugs/closed/2613.v index 4f0470b1df..15f3bf52c3 100644 --- a/test-suite/bugs/closed/2613.v +++ b/test-suite/bugs/closed/2613.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *) Require Import ZArith. diff --git a/test-suite/bugs/closed/2615.v b/test-suite/bugs/closed/2615.v index dde6a6a5ed..38c1cfc848 100644 --- a/test-suite/bugs/closed/2615.v +++ b/test-suite/bugs/closed/2615.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* This failed with an anomaly in pre-8.4 because of let-in not properly taken into account in the test for unification pattern *) diff --git a/test-suite/bugs/closed/2883.v b/test-suite/bugs/closed/2883.v index 5a5d90a403..f027b5eb29 100644 --- a/test-suite/bugs/closed/2883.v +++ b/test-suite/bugs/closed/2883.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Import List. Require Import Coq.Program.Equality. diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v index ff75a1f320..a03adbd73c 100644 --- a/test-suite/bugs/closed/2969.v +++ b/test-suite/bugs/closed/2969.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* Check that Goal.V82.byps and Goal.V82.env are consistent *) (* This is a shorten variant of the initial bug which raised anomaly *) diff --git a/test-suite/bugs/closed/2996.v b/test-suite/bugs/closed/2996.v index 440cda6176..d5409289c5 100644 --- a/test-suite/bugs/closed/2996.v +++ b/test-suite/bugs/closed/2996.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* Test on definitions referring to section variables that are not any longer in the current context *) diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v index 03e5af61b9..ced6d95949 100644 --- a/test-suite/bugs/closed/3068.v +++ b/test-suite/bugs/closed/3068.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Section Counted_list. Variable A : Type. diff --git a/test-suite/bugs/closed/3258.v b/test-suite/bugs/closed/3258.v index a1390e3025..b263c6baf4 100644 --- a/test-suite/bugs/closed/3258.v +++ b/test-suite/bugs/closed/3258.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Import Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Program.Program Coq.Setoids.Setoid. Global Set Implicit Arguments. diff --git a/test-suite/bugs/closed/3259.v b/test-suite/bugs/closed/3259.v index 0306c68667..aa91fc3de7 100644 --- a/test-suite/bugs/closed/3259.v +++ b/test-suite/bugs/closed/3259.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Goal forall m n, n+n = m+m -> m+m = m+m. Proof. intros. diff --git a/test-suite/bugs/closed/3298.v b/test-suite/bugs/closed/3298.v index 3a7de45670..f07ee1e6cf 100644 --- a/test-suite/bugs/closed/3298.v +++ b/test-suite/bugs/closed/3298.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Module JGross. Hint Extern 1 => match goal with |- match ?E with end => case E end. diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v index 049589325e..980431576c 100644 --- a/test-suite/bugs/closed/3309.v +++ b/test-suite/bugs/closed/3309.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- coq-prog-args: ("-emacs" "-impredicative-set") -*- *) (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v index 647862637a..e63c46da04 100644 --- a/test-suite/bugs/closed/3314.v +++ b/test-suite/bugs/closed/3314.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Universe Polymorphism. Definition Lift : $(let U1 := constr:(Type) in diff --git a/test-suite/bugs/closed/3319.v b/test-suite/bugs/closed/3319.v index bb5853ddd3..3b37e39e52 100644 --- a/test-suite/bugs/closed/3319.v +++ b/test-suite/bugs/closed/3319.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5353 lines to 4545 lines, then from 4513 lines to 4504 lines, then from 4515 lines to 4508 lines, then from 4519 lines to 132 lines, then from 111 lines to 66 lines, then from 68 lines to 35 lines *) Set Implicit Arguments. Inductive paths {A : Type} (a : A) : A -> Type := diff --git a/test-suite/bugs/closed/3321.v b/test-suite/bugs/closed/3321.v index 07e3b3cb50..b6f10e533e 100644 --- a/test-suite/bugs/closed/3321.v +++ b/test-suite/bugs/closed/3321.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5302 lines to 4649 lines, then from 4660 lines to 355 lines, then from 360 lines to 269 lines, then from 269 lines to 175 lines, then from 144 lines to 119 lines, then from 103 lines to 83 lines, then from 86 lines to 36 lines, then from 37 lines to 17 lines *) Axiom admit : forall {T}, T. diff --git a/test-suite/bugs/closed/3322.v b/test-suite/bugs/closed/3322.v index 925f22a211..ab3025a6aa 100644 --- a/test-suite/bugs/closed/3322.v +++ b/test-suite/bugs/closed/3322.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 11971 lines to 11753 lines, then from 7702 lines to 564 lines, then from 571 lines to 61 lines *) Set Asymmetric Patterns. Axiom admit : forall {T}, T. diff --git a/test-suite/bugs/closed/3323.v b/test-suite/bugs/closed/3323.v index fb5a8a7eb6..22b1603b60 100644 --- a/test-suite/bugs/closed/3323.v +++ b/test-suite/bugs/closed/3323.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 5302 lines to 4649 lines, then from 4660 lines to 355 lines, then from 360 lines to 269 lines, then from 269 lines to 175 lines, then from 144 lines to 119 lines, then from 297 lines to 117 lines, then from 95 lines to 79 lines, then from 82 lines to 68 lines *) diff --git a/test-suite/bugs/closed/3324.v b/test-suite/bugs/closed/3324.v index 9cd6e4c2e0..45dbb57aa2 100644 --- a/test-suite/bugs/closed/3324.v +++ b/test-suite/bugs/closed/3324.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Module ETassi. Axiom admit : forall {T}, T. Class IsHProp (A : Type) : Type := {}. diff --git a/test-suite/bugs/closed/3329.v b/test-suite/bugs/closed/3329.v index f7e368f8f4..ecb09e8436 100644 --- a/test-suite/bugs/closed/3329.v +++ b/test-suite/bugs/closed/3329.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12095 lines to 869 lines, then from 792 lines to 504 lines, then from 487 lines to 353 lines, then from 258 lines to 174 lines, then from 164 lines to 132 lines, then from 129 lines to 99 lines *) Set Universe Polymorphism. Generalizable All Variables. diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index 15303cca45..4cd7c39e88 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *) Set Universe Polymorphism. Definition setleq (A : Type@{i}) (B : Type@{j}) := A : Type@{j}. diff --git a/test-suite/bugs/closed/3344.v b/test-suite/bugs/closed/3344.v index 8255fd6cce..880851c565 100644 --- a/test-suite/bugs/closed/3344.v +++ b/test-suite/bugs/closed/3344.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 716 lines to 197 lines, then from 206 lines to 162 lines, then from 163 lines to 73 lines *) Require Import Coq.Sets.Ensembles. Require Import Coq.Strings.String. diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v index 37c0d87eec..63d5c7a57b 100644 --- a/test-suite/bugs/closed/3347.v +++ b/test-suite/bugs/closed/3347.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *) Set Universe Polymorphism. Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing). diff --git a/test-suite/bugs/closed/3350.v b/test-suite/bugs/closed/3350.v index 30fdf16940..c041c401fd 100644 --- a/test-suite/bugs/closed/3350.v +++ b/test-suite/bugs/closed/3350.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Coq.Vectors.Fin. Require Coq.Vectors.Vector. diff --git a/test-suite/bugs/closed/3373.v b/test-suite/bugs/closed/3373.v index 5ecf280153..051e695203 100644 --- a/test-suite/bugs/closed/3373.v +++ b/test-suite/bugs/closed/3373.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then diff --git a/test-suite/bugs/closed/3374.v b/test-suite/bugs/closed/3374.v index 3c67703a2b..d8e72f4f20 100644 --- a/test-suite/bugs/closed/3374.v +++ b/test-suite/bugs/closed/3374.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 331 lines to 59 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3375.v b/test-suite/bugs/closed/3375.v index fe323fcb28..d7ce02ea87 100644 --- a/test-suite/bugs/closed/3375.v +++ b/test-suite/bugs/closed/3375.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *) (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 330 lines to 45 lines *) diff --git a/test-suite/bugs/closed/3382.v b/test-suite/bugs/closed/3382.v index 1d8e916747..3e374d9077 100644 --- a/test-suite/bugs/closed/3382.v +++ b/test-suite/bugs/closed/3382.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines, then from 139 lines to 114 lines, then from 93 lines to 77 lines *) Set Implicit Arguments. diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v index 02eca64eea..3a59869546 100644 --- a/test-suite/bugs/closed/3392.v +++ b/test-suite/bugs/closed/3392.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12105 lines to 142 lines, then from 83 lines to 57 lines *) Generalizable All Variables. Axiom admit : forall {T}, T. diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v index ec25e68297..f7ab5f76a5 100644 --- a/test-suite/bugs/closed/3393.v +++ b/test-suite/bugs/closed/3393.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 8760 lines to 7519 lines, then from 7050 lines to 909 lines, then from 846 lines to 578 lines, then from 497 lines to 392 lines, then from 365 lines to 322 lines, then from 252 lines to 205 lines, then from 215 lines to 204 lines, then from 210 lines to 182 lines, then from 175 lines to 157 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3422.v b/test-suite/bugs/closed/3422.v index d984f6230d..460ae8f110 100644 --- a/test-suite/bugs/closed/3422.v +++ b/test-suite/bugs/closed/3422.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Generalizable All Variables. Set Implicit Arguments. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3427.v b/test-suite/bugs/closed/3427.v index 8483a4ecf4..374a53928d 100644 --- a/test-suite/bugs/closed/3427.v +++ b/test-suite/bugs/closed/3427.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 0 lines to 7171 lines, then from 7184 lines to 558 lines, then from 556 lines to 209 lines *) Generalizable All Variables. diff --git a/test-suite/bugs/closed/3439.v b/test-suite/bugs/closed/3439.v index bba6140f70..1ea24bf1b8 100644 --- a/test-suite/bugs/closed/3439.v +++ b/test-suite/bugs/closed/3439.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 3154 lines to 149 lines, then from 89 lines to 55 lines, then from 44 lines to 20 lines *) Set Primitive Projections. Generalizable All Variables. diff --git a/test-suite/bugs/closed/3480.v b/test-suite/bugs/closed/3480.v index 99ac2efab1..a81837e714 100644 --- a/test-suite/bugs/closed/3480.v +++ b/test-suite/bugs/closed/3480.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Primitive Projections. Axiom admit : forall {T}, T. Notation "( x ; y )" := (existT _ x y) : fibration_scope. diff --git a/test-suite/bugs/closed/3484.v b/test-suite/bugs/closed/3484.v index 6c40a4266a..dc88a332b4 100644 --- a/test-suite/bugs/closed/3484.v +++ b/test-suite/bugs/closed/3484.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 14259 lines to 305 lines, then from 237 lines to 120 lines, then from 100 lines to 30 lines *) Set Primitive Projections. Set Implicit Arguments. diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 80695f382c..fcdfa0057b 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *) Require Coq.Setoids.Setoid. Import Coq.Setoids.Setoid. diff --git a/test-suite/bugs/closed/3531.v b/test-suite/bugs/closed/3531.v index fd080a6b0e..764a7334e8 100644 --- a/test-suite/bugs/closed/3531.v +++ b/test-suite/bugs/closed/3531.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 270 lines to 198 lines, then from 178 lines to 82 lines, then from 88 lines to 59 lines *) (* coqc version trunk (August 2014) compiled on Aug 19 2014 14:40:15 with OCaml diff --git a/test-suite/bugs/closed/3561.v b/test-suite/bugs/closed/3561.v index b4dfd17f50..f6cbc92992 100644 --- a/test-suite/bugs/closed/3561.v +++ b/test-suite/bugs/closed/3561.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 6343 lines to 2362 lines, then from 2115 lines to 303 lines, then from 321 lines to 90 lines, then from 95 lines to 41 lines *) (* coqc version trunk (August 2014) compiled on Aug 31 2014 10:12:32 with OCaml 4.01.0 coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (437b91a3ffd7327975a129b95b24d3f66ad7f3e4) *) diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v index 51d6744c5c..3440f0e806 100644 --- a/test-suite/bugs/closed/3590.v +++ b/test-suite/bugs/closed/3590.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* Set Primitive Projections. *) Set Implicit Arguments. Record prod A B := pair { fst : A ; snd : B }. diff --git a/test-suite/bugs/closed/3596.v b/test-suite/bugs/closed/3596.v index d6c1c949de..49dd7be5a8 100644 --- a/test-suite/bugs/closed/3596.v +++ b/test-suite/bugs/closed/3596.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Implicit Arguments. Record foo := { fx : nat }. Set Primitive Projections. diff --git a/test-suite/bugs/closed/3625.v b/test-suite/bugs/closed/3625.v index 3d30b62f80..d4b2cc5ccc 100644 --- a/test-suite/bugs/closed/3625.v +++ b/test-suite/bugs/closed/3625.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Implicit Arguments. Set Primitive Projections. Record prod A B := pair { fst : A ; snd : B }. diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v index cd542c8a57..495e67e09e 100644 --- a/test-suite/bugs/closed/3647.v +++ b/test-suite/bugs/closed/3647.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Coq.Setoids.Setoid. Axiom BITS : nat -> Set. diff --git a/test-suite/bugs/closed/3653.v b/test-suite/bugs/closed/3653.v index 947b36017f..b97689676b 100644 --- a/test-suite/bugs/closed/3653.v +++ b/test-suite/bugs/closed/3653.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Setoid. Variables P Q : forall {T : Set}, T -> Prop. diff --git a/test-suite/bugs/closed/3658.v b/test-suite/bugs/closed/3658.v index b1158b9a42..622c3c94ac 100644 --- a/test-suite/bugs/closed/3658.v +++ b/test-suite/bugs/closed/3658.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12178 lines to 457 lines, then from 500 lines to 147 lines, then from 175 lines to 56 lines *) (* coqc version trunk (September 2014) compiled on Sep 21 2014 16:34:4 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (eaf864354c3fda9ddc1f03f0b1c7807b6fd44322) *) diff --git a/test-suite/bugs/closed/3660.v b/test-suite/bugs/closed/3660.v index ed8964ce11..39eb89c402 100644 --- a/test-suite/bugs/closed/3660.v +++ b/test-suite/bugs/closed/3660.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Generalizable All Variables. Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. diff --git a/test-suite/bugs/closed/3664.v b/test-suite/bugs/closed/3664.v index 41de74ff35..63a81b6d01 100644 --- a/test-suite/bugs/closed/3664.v +++ b/test-suite/bugs/closed/3664.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Module NonPrim. Unset Primitive Projections. Record c := { d : Set }. diff --git a/test-suite/bugs/closed/3668.v b/test-suite/bugs/closed/3668.v index 547159b954..da01ed00e4 100644 --- a/test-suite/bugs/closed/3668.v +++ b/test-suite/bugs/closed/3668.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 6329 lines to 110 lines, then from 115 lines to 88 lines, then from 93 lines to 72 lines *) (* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *) diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v index b8c5b4d524..2a282d221f 100644 --- a/test-suite/bugs/closed/3682.v +++ b/test-suite/bugs/closed/3682.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Class Foo. Definition bar `{Foo} (x : Set) := Set. Instance: Foo. diff --git a/test-suite/bugs/closed/3684.v b/test-suite/bugs/closed/3684.v index 94ce4a608f..f7b137386b 100644 --- a/test-suite/bugs/closed/3684.v +++ b/test-suite/bugs/closed/3684.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Definition foo : Set. Proof. refine ($(abstract admit)$). diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v index ee6b334ba2..b650920b26 100644 --- a/test-suite/bugs/closed/3686.v +++ b/test-suite/bugs/closed/3686.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Universe Polymorphism. Set Implicit Arguments. Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. diff --git a/test-suite/bugs/closed/3698.v b/test-suite/bugs/closed/3698.v index 3c53d243ed..31de8ec45b 100644 --- a/test-suite/bugs/closed/3698.v +++ b/test-suite/bugs/closed/3698.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5479 lines to 4682 lines, then from 4214 lines to 86 lines, then from 60 lines to 25 lines *) (* coqc version trunk (October 2014) compiled on Oct 1 2014 18:13:54 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (68846802a7be637ec805a5e374655a426b5723a5) *) diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 99b3d79e19..62137f0c06 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 9593 lines to 104 lines, then from 187 lines to 103 lines, then from 113 lines to 90 lines *) (* coqc version trunk (October 2014) compiled on Oct 1 2014 18:13:54 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (68846802a7be637ec805a5e374655a426b5723a5) *) diff --git a/test-suite/bugs/closed/3703.v b/test-suite/bugs/closed/3703.v index 8f7fe0a09f..7282500769 100644 --- a/test-suite/bugs/closed/3703.v +++ b/test-suite/bugs/closed/3703.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 6746 lines to 4190 lines, then from 29 lines to 18 lines, then fro\ m 30 lines to 19 lines *) (* coqc version trunk (October 2014) compiled on Oct 7 2014 12:42:41 with OCaml 4.01.0 diff --git a/test-suite/bugs/closed/3709.v b/test-suite/bugs/closed/3709.v index 7f01be7abd..815f5b9507 100644 --- a/test-suite/bugs/closed/3709.v +++ b/test-suite/bugs/closed/3709.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Module NonPrim. Unset Primitive Projections. Record hProp := hp { hproptype :> Type }. diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v index 6e5952a527..76beedf687 100644 --- a/test-suite/bugs/closed/3732.v +++ b/test-suite/bugs/closed/3732.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 2073 lines to 358 lines, then from 359 lines to 218 lines, then from 107 lines to 92 lines *) (* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *) diff --git a/test-suite/bugs/closed/3782.v b/test-suite/bugs/closed/3782.v index 08d456fc6d..2dc50c17d0 100644 --- a/test-suite/bugs/closed/3782.v +++ b/test-suite/bugs/closed/3782.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 2674 lines to 136 lines, then from 115 lines to 61 lines *) (* coqc version trunk (October 2014) compiled on Oct 28 2014 14:33:38 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,(no branch) (53bfe9cf58a3c40e6eb7120d25c1633a9cea3126) *) diff --git a/test-suite/bugs/closed/3783.v b/test-suite/bugs/closed/3783.v index 33ca9651a5..e217129688 100644 --- a/test-suite/bugs/closed/3783.v +++ b/test-suite/bugs/closed/3783.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Fixpoint exp (n : nat) (T : Set) := match n with | 0 => T diff --git a/test-suite/bugs/closed/3786.v b/test-suite/bugs/closed/3786.v index fd3bd7bd76..23d19e946f 100644 --- a/test-suite/bugs/closed/3786.v +++ b/test-suite/bugs/closed/3786.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Coq.Lists.List. Require Coq.Sets.Ensembles. Import Coq.Sets.Ensembles. diff --git a/test-suite/bugs/closed/3798.v b/test-suite/bugs/closed/3798.v index 623822e990..b9f0daa71c 100644 --- a/test-suite/bugs/closed/3798.v +++ b/test-suite/bugs/closed/3798.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Setoid. Parameter f : nat -> nat. diff --git a/test-suite/bugs/closed/3854.v b/test-suite/bugs/closed/3854.v index f8329cdd20..7e915f202b 100644 --- a/test-suite/bugs/closed/3854.v +++ b/test-suite/bugs/closed/3854.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Definition relation (A : Type) := A -> A -> Type. Class Reflexive {A} (R : relation A) := reflexivity : forall x : A, R x x. Axiom IsHProp : Type -> Type. diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v index 6b52411752..9320848910 100644 --- a/test-suite/bugs/closed/3922.v +++ b/test-suite/bugs/closed/3922.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Universe Polymorphism. Notation Type0 := Set. diff --git a/test-suite/bugs/closed/3938.v b/test-suite/bugs/closed/3938.v index 9844313383..859e9f0177 100644 --- a/test-suite/bugs/closed/3938.v +++ b/test-suite/bugs/closed/3938.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Import Coq.Arith.PeanoNat. Hint Extern 1 => admit : typeclass_instances. Require Import Setoid. diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index 0ccbf5652f..1449f242b4 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *) (* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0 diff --git a/test-suite/bugs/closed/4097.v b/test-suite/bugs/closed/4097.v index 2109a4cd92..02aa25e09f 100644 --- a/test-suite/bugs/closed/4097.v +++ b/test-suite/bugs/closed/4097.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 6082 lines to 81 lines, then from 436 lines to 93 lines *) (* coqc version 8.5beta1 (February 2015) compiled on Feb 27 2015 15:10:37 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (fc1b3ef9d7270938cd83c524aae0383093b7a4b5) *) diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v index 8592c729d0..0b8bb23534 100644 --- a/test-suite/bugs/closed/HoTT_coq_007.v +++ b/test-suite/bugs/closed/HoTT_coq_007.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Module Comment1. Set Implicit Arguments. diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v index 63548a644d..d00a707bd5 100644 --- a/test-suite/bugs/closed/HoTT_coq_014.v +++ b/test-suite/bugs/closed/HoTT_coq_014.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Implicit Arguments. Generalizable All Variables. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index b16c1df2bd..4938b80f9b 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Implicit Arguments. Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_029.v b/test-suite/bugs/closed/HoTT_coq_029.v index 4fd54b5699..161c4d21ec 100644 --- a/test-suite/bugs/closed/HoTT_coq_029.v +++ b/test-suite/bugs/closed/HoTT_coq_029.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Module FirstComment. Set Implicit Arguments. Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_030.v b/test-suite/bugs/closed/HoTT_coq_030.v index fa5ee25cae..9f89248348 100644 --- a/test-suite/bugs/closed/HoTT_coq_030.v +++ b/test-suite/bugs/closed/HoTT_coq_030.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. diff --git a/test-suite/bugs/closed/HoTT_coq_035.v b/test-suite/bugs/closed/HoTT_coq_035.v index 4ad2fc0236..133bf6c732 100644 --- a/test-suite/bugs/closed/HoTT_coq_035.v +++ b/test-suite/bugs/closed/HoTT_coq_035.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Fail Check Prop : Prop. (* Prop:Prop : Prop *) Fail Check Set : Prop. (* Set:Prop diff --git a/test-suite/bugs/closed/HoTT_coq_042.v b/test-suite/bugs/closed/HoTT_coq_042.v index 6b206a2f58..432cf7054f 100644 --- a/test-suite/bugs/closed/HoTT_coq_042.v +++ b/test-suite/bugs/closed/HoTT_coq_042.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Implicit Arguments. Set Universe Polymorphism. Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_055.v b/test-suite/bugs/closed/HoTT_coq_055.v index 92d70ad139..a250987714 100644 --- a/test-suite/bugs/closed/HoTT_coq_055.v +++ b/test-suite/bugs/closed/HoTT_coq_055.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v index 6e65320d15..3e3a987a7c 100644 --- a/test-suite/bugs/closed/HoTT_coq_056.v +++ b/test-suite/bugs/closed/HoTT_coq_056.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 10455 lines to 8350 lines, then from 7790 lines to 710 lines, then from 7790 lines to 710 lines, then from 566 lines to 340 lines, then from 191 lines to 171 lines, then from 191 lines to 171 lines. *) Set Implicit Arguments. diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v index 9ce7dba974..5e5d5ab3e7 100644 --- a/test-suite/bugs/closed/HoTT_coq_058.v +++ b/test-suite/bugs/closed/HoTT_coq_058.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 10044 lines to 493 lines, then from 425 lines to 160 lines. *) Set Universe Polymorphism. Notation idmap := (fun x => x). diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v index 26c1f963d3..19551dc92e 100644 --- a/test-suite/bugs/closed/HoTT_coq_061.v +++ b/test-suite/bugs/closed/HoTT_coq_061.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* There are some problems in materialize_evar with local definitions, as CO below; this is not completely sorted out yet, but at least it fails in a smooth way at the time of today [HH] *) diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v index db89531682..b7db22a69e 100644 --- a/test-suite/bugs/closed/HoTT_coq_062.v +++ b/test-suite/bugs/closed/HoTT_coq_062.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v index 5f0a541b0e..b4c745375f 100644 --- a/test-suite/bugs/closed/HoTT_coq_064.v +++ b/test-suite/bugs/closed/HoTT_coq_064.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 279 lines to 219 lines. *) Set Implicit Arguments. diff --git a/test-suite/bugs/closed/HoTT_coq_067.v b/test-suite/bugs/closed/HoTT_coq_067.v index ad32a60c65..84a5bc029f 100644 --- a/test-suite/bugs/closed/HoTT_coq_067.v +++ b/test-suite/bugs/closed/HoTT_coq_067.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Universe Polymorphism. Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. diff --git a/test-suite/bugs/closed/HoTT_coq_088.v b/test-suite/bugs/closed/HoTT_coq_088.v index b3e1df5796..0428af0d44 100644 --- a/test-suite/bugs/closed/HoTT_coq_088.v +++ b/test-suite/bugs/closed/HoTT_coq_088.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v index 5c7041471c..5fa167038d 100644 --- a/test-suite/bugs/closed/HoTT_coq_090.v +++ b/test-suite/bugs/closed/HoTT_coq_090.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (** I'm not sure if this tests what I want it to test... *) Set Implicit Arguments. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v index fc99daab68..bdcd8ba97d 100644 --- a/test-suite/bugs/closed/HoTT_coq_098.v +++ b/test-suite/bugs/closed/HoTT_coq_098.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Implicit Arguments. Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_099.v b/test-suite/bugs/closed/HoTT_coq_099.v index 9b6ace824c..cd5b0c8ff6 100644 --- a/test-suite/bugs/closed/HoTT_coq_099.v +++ b/test-suite/bugs/closed/HoTT_coq_099.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 138 lines to 78 lines. *) Set Implicit Arguments. Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_100.v b/test-suite/bugs/closed/HoTT_coq_100.v index c39b709342..663b6280e4 100644 --- a/test-suite/bugs/closed/HoTT_coq_100.v +++ b/test-suite/bugs/closed/HoTT_coq_100.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 335 lines to 115 lines. *) Set Implicit Arguments. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_101.v b/test-suite/bugs/closed/HoTT_coq_101.v index 9c89a6ab9d..3ef56892be 100644 --- a/test-suite/bugs/closed/HoTT_coq_101.v +++ b/test-suite/bugs/closed/HoTT_coq_101.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_102.v b/test-suite/bugs/closed/HoTT_coq_102.v index 71becfd2e5..996aaaa492 100644 --- a/test-suite/bugs/closed/HoTT_coq_102.v +++ b/test-suite/bugs/closed/HoTT_coq_102.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 64 lines to 30 lines. *) Set Implicit Arguments. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index c3a83627ee..9a1da16bf6 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -59,7 +59,7 @@ Instance trunc_sigma `{P : A -> Type} Proof. generalize dependent A. - induction n; [ | admit ]; simpl; intros A P ac Pc. + induction n; [ | apply admit ]; simpl; intros A P ac Pc. (exists (existT _ (center A) (center (P (center A))))). intros [a ?]. refine (path_sigma' P (contr a) (path_contr _ _)). @@ -102,5 +102,5 @@ The term | false => B end))" (Universe inconsistency: Cannot enforce Top.197 = Set)). *) - admit. + apply admit. Defined. diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v index cc30480273..4f5ef99740 100644 --- a/test-suite/bugs/closed/HoTT_coq_108.v +++ b/test-suite/bugs/closed/HoTT_coq_108.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *) (* File reduced by coq-bug-finder from 139 lines to 124 lines. *) diff --git a/test-suite/bugs/closed/HoTT_coq_112.v b/test-suite/bugs/closed/HoTT_coq_112.v index 150f2ecc89..5bee69fcde 100644 --- a/test-suite/bugs/closed/HoTT_coq_112.v +++ b/test-suite/bugs/closed/HoTT_coq_112.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 4464 lines to 4137 lines, then from 3683 lines to 118 lines, then from 124 lines to 75 lines. *) Set Universe Polymorphism. Definition admit {T} : T. diff --git a/test-suite/bugs/closed/HoTT_coq_113.v b/test-suite/bugs/closed/HoTT_coq_113.v index 3ef531bc96..05e767840e 100644 --- a/test-suite/bugs/closed/HoTT_coq_113.v +++ b/test-suite/bugs/closed/HoTT_coq_113.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 3329 lines to 153 lines, then from 118 lines to 49 lines, then from 55 lines to 38 lines, then from 46 lines to 16 lines *) Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_118.v b/test-suite/bugs/closed/HoTT_coq_118.v index 14ad0e49d2..e41689cba3 100644 --- a/test-suite/bugs/closed/HoTT_coq_118.v +++ b/test-suite/bugs/closed/HoTT_coq_118.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5631 lines to 557 lines, then from 526 lines to 181 lines, then from 189 lines to 154 lines, then from 153 lines to 107 lines, then from 97 lines to 56 lines, then from 50 lines to 37 lines *) Generalizable All Variables. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_121.v b/test-suite/bugs/closed/HoTT_coq_121.v index cce288cffa..90493a530c 100644 --- a/test-suite/bugs/closed/HoTT_coq_121.v +++ b/test-suite/bugs/closed/HoTT_coq_121.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines, then from 146 lines to 72 lines, then from 82 lines to 70 lines, then from 79 lines to 49 lines, then from 59 lines to 16 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index 994dff637f..6ee6e65323 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") *) (* File reduced by coq-bug-finder from original input, then from 4988 lines to 856 lines, then from 648 lines to 398 lines, then from 401 lines to 332 lines, then from 287 lines to 250 lines, then from 257 lines to 241 lines, then from 223 lines to 175 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v index 6de13f74e3..f0c707bd10 100644 --- a/test-suite/bugs/opened/3263.v +++ b/test-suite/bugs/opened/3263.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) Generalizable All Variables. Set Implicit Arguments. diff --git a/test-suite/bugs/opened/3345.v b/test-suite/bugs/opened/3345.v index b61174a865..3e3da6df71 100644 --- a/test-suite/bugs/opened/3345.v +++ b/test-suite/bugs/opened/3345.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 1972 lines to 136 lines, then from 119 lines to 105 lines *) Global Set Implicit Arguments. Require Import Coq.Lists.List Program. diff --git a/test-suite/bugs/opened/3395.v b/test-suite/bugs/opened/3395.v index ff0dbf9745..5ca48fc9d6 100644 --- a/test-suite/bugs/opened/3395.v +++ b/test-suite/bugs/opened/3395.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) Generalizable All Variables. Set Implicit Arguments. diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v index 02e47a8b48..3913bbb43f 100644 --- a/test-suite/bugs/opened/3509.v +++ b/test-suite/bugs/opened/3509.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Lemma match_bool_fn b A B xT xF : match b as b return forall x : A, B b x with | true => xT diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v index 25285636b3..daf265071a 100644 --- a/test-suite/bugs/opened/3510.v +++ b/test-suite/bugs/opened/3510.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Lemma match_option_fn T (b : option T) A B s n : match b as b return forall x : A, B b x with | Some k => s k diff --git a/test-suite/bugs/opened/3685.v b/test-suite/bugs/opened/3685.v index d647b5a83d..b2b5db6be7 100644 --- a/test-suite/bugs/opened/3685.v +++ b/test-suite/bugs/opened/3685.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Set Universe Polymorphism. Class Funext := { }. Delimit Scope category_scope with category. diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v index c744188201..9b3f94d917 100644 --- a/test-suite/bugs/opened/3754.v +++ b/test-suite/bugs/opened/3754.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *) (* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1 coqtop version trunk (October 2014) *) diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v index 9413daa041..a03e8ffdab 100644 --- a/test-suite/bugs/opened/3848.v +++ b/test-suite/bugs/opened/3848.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y. Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing). Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x. diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v index 7847c5e441..05ee6c7b60 100644 --- a/test-suite/bugs/opened/HoTT_coq_120.v +++ b/test-suite/bugs/opened/HoTT_coq_120.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *) Set Universe Polymorphism. Generalizable All Variables. diff --git a/test-suite/ide/undo020.fake b/test-suite/ide/undo020.fake index 2adde908dd..aa1d9bb2a7 100644 --- a/test-suite/ide/undo020.fake +++ b/test-suite/ide/undo020.fake @@ -12,8 +12,8 @@ ADD { Qed. } # second proof ADD { Lemma b : False. } ADD { Proof using. } -ADD { admit. } -ADD last { Qed. } +ADD { give_up. } +ADD last { Admitted. } # We join and expect some proof to fail WAIT # Going back to the error diff --git a/test-suite/prerequisite/admit.v b/test-suite/prerequisite/admit.v new file mode 100644 index 0000000000..fb3276632d --- /dev/null +++ b/test-suite/prerequisite/admit.v @@ -0,0 +1,2 @@ +Axiom proof_admitted : False. +Ltac admit := case proof_admitted. diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v index d819dc47aa..563339739e 100644 --- a/test-suite/success/AdvancedCanonicalStructure.v +++ b/test-suite/success/AdvancedCanonicalStructure.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Section group_morphism. (* An example with default canonical structures *) diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index d316e4a09c..e38affd7fa 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* compile en user 3m39.915s sur cachalot *) Require Import Nsatz. diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index dbbd57ae0d..61e73f8587 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Section Foo. Variable a : nat. diff --git a/test-suite/success/rewrite_dep.v b/test-suite/success/rewrite_dep.v index fe250ae882..d0aafd3833 100644 --- a/test-suite/success/rewrite_dep.v +++ b/test-suite/success/rewrite_dep.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Import Setoid. Require Import Morphisms. Require Vector. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index be0d49e008..0465c4b3fb 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. Require Import Setoid. Parameter A : Set. diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index b533077962..e540ae5f30 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* Check that inversion of names of mutual inductive fixpoints works *) (* (cf bug #1031) *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index d2971552d4..50f853f0e0 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -22,9 +22,6 @@ Inductive True : Prop := (** [False] is the always false proposition *) Inductive False : Prop :=. -(** [proof_admitted] is used to implement the admit tactic *) -Axiom proof_admitted : False. - (** [not A], written [~A], is the negation of [A] *) Definition not (A:Prop) := A -> False. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 4894eba4ba..0efb8744d8 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -23,4 +23,4 @@ Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". Declare ML Module "recdef_plugin". (* Default substrings not considered by queries like SearchAbout *) -Add Search Blacklist "_admitted" "_subproof" "Private_". +Add Search Blacklist "_subproof" "Private_". |