aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-ext.tex1
-rw-r--r--interp/constrextern.ml11
-rw-r--r--kernel/univ.ml6
-rw-r--r--library/declare.ml2
-rw-r--r--library/universes.ml4
-rw-r--r--parsing/tok.ml1
-rw-r--r--pretyping/pretyping.ml30
-rw-r--r--proofs/pfedit.ml10
-rw-r--r--proofs/pfedit.mli7
-rw-r--r--proofs/proof_global.ml28
-rw-r--r--proofs/proof_global.mli17
-rw-r--r--stm/lemmas.ml63
-rw-r--r--stm/lemmas.mli17
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--test-suite/bugs/closed/3735.v4
-rw-r--r--test-suite/bugs/closed/3807.v33
-rw-r--r--test-suite/bugs/closed/4284.v6
-rw-r--r--test-suite/bugs/closed/4287.v6
-rw-r--r--test-suite/bugs/closed/4400.v19
-rw-r--r--test-suite/bugs/closed/4433.v29
-rw-r--r--test-suite/success/Notations.v6
-rw-r--r--theories/Classes/CMorphisms.v14
-rw-r--r--theories/Logic/ClassicalFacts.v1
-rw-r--r--theories/Logic/Hurkens.v121
-rw-r--r--toplevel/command.ml6
-rw-r--r--toplevel/obligations.ml4
-rw-r--r--toplevel/vernacentries.ml6
27 files changed, 307 insertions, 147 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index d21c91201..b77118e1f 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -253,6 +253,7 @@ Reset Initial.
\Rem An experimental syntax for projections based on a dot notation is
available. The command to activate it is
+\optindex{Printing Projections}
\begin{quote}
{\tt Set Printing Projections.}
\end{quote}
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f57772ecb..5160f07af 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -147,8 +147,17 @@ let extern_evar loc n l = CEvar (loc,n,l)
For instance, in the debugger the tables of global references
may be inaccurate *)
+let safe_shortest_qualid_of_global vars r =
+ try shortest_qualid_of_global vars r
+ with Not_found ->
+ match r with
+ | VarRef v -> make_qualid DirPath.empty v
+ | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c))
+ | IndRef (i,_) | ConstructRef ((i,_),_) ->
+ make_qualid DirPath.empty Names.(Label.to_id (mind_label i))
+
let default_extern_reference loc vars r =
- Qualid (loc,shortest_qualid_of_global vars r)
+ Qualid (loc,safe_shortest_qualid_of_global vars r)
let my_extern_reference = ref default_extern_reference
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 4cc34e41e..fab0e6fb8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,7 +937,9 @@ struct
else if Array.length y = 0 then x
else Array.append x y
- let of_array a = a
+ let of_array a =
+ assert(Array.for_all (fun x -> not (Level.is_prop x)) a);
+ a
let to_array a = a
@@ -945,7 +947,7 @@ struct
let subst_fn fn t =
let t' = CArray.smartmap fn t in
- if t' == t then t else t'
+ if t' == t then t else of_array t'
let levels x = LSet.of_array x
diff --git a/library/declare.ml b/library/declare.ml
index 5968fbf38..994a6557a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -431,7 +431,7 @@ let cache_universes (p, l) =
Univ.ContextSet.add_universe lev ctx))
(glob, Univ.ContextSet.empty) l
in
- Global.push_context_set false ctx;
+ Global.push_context_set p ctx;
if p then Lib.add_section_context ctx;
Universes.set_global_universe_names glob'
diff --git a/library/universes.ml b/library/universes.ml
index a157a747c..96937b3b3 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -815,7 +815,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
let cstrs' = List.fold_left (fun cstrs (d, r) ->
if d == Univ.Le then
enforce_leq inst (Universe.make r) cstrs
- else
+ else
try let lev = Option.get (Universe.level inst) in
Constraint.add (lev, d, r) cstrs
with Option.IsNone -> failwith "")
@@ -849,7 +849,7 @@ let normalize_context_set ctx us algs =
Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
if d == Le then
if Univ.Level.is_small l then
- if is_set_minimization () then
+ if is_set_minimization () && LSet.mem r ctx then
(Constraint.add cstr smallles, noneqs)
else (smallles, noneqs)
else if Level.is_small r then
diff --git a/parsing/tok.ml b/parsing/tok.ml
index efd57968d..12140f403 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -21,6 +21,7 @@ type t =
| EOI
let equal t1 t2 = match t1, t2 with
+| IDENT s1, KEYWORD s2 -> CString.equal s1 s2
| KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
| METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2
| PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5f657aff5..78f134248 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -394,18 +394,22 @@ let pretype_global loc rigid env evd gr us =
match us with
| None -> evd, None
| Some l ->
- let _, ctx = Universes.unsafe_constr_of_global gr in
- let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
- let len = Array.length arr in
- if len != List.length l then
- user_err_loc (loc, "pretype",
- str "Universe instance should have length " ++ int len)
- else
- let evd, l' = List.fold_left (fun (evd, univs) l ->
+ let _, ctx = Universes.unsafe_constr_of_global gr in
+ let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
+ let len = Array.length arr in
+ if len != List.length l then
+ user_err_loc (loc, "pretype",
+ str "Universe instance should have length " ++ int len)
+ else
+ let evd, l' = List.fold_left (fun (evd, univs) l ->
let evd, l = interp_universe_level_name evd l in
(evd, l :: univs)) (evd, []) l
- in
- evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+ in
+ if List.exists (fun l -> Univ.Level.is_prop l) l' then
+ user_err_loc (loc, "pretype",
+ str "Universe instances cannot contain Prop, polymorphic" ++
+ str " universe instances must be greater or equal to Set.");
+ evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
in
Evd.fresh_global ~rigid ?names:instance env evd gr
@@ -440,13 +444,15 @@ let pretype_sort evdref = function
let new_type_evar env evdref loc =
let e, s =
- evd_comb0 (fun evd -> Evarutil.new_type_evar env evd univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
+ evd_comb0 (fun evd -> Evarutil.new_type_evar env evd
+ univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
in e
let get_projection env cst =
let cb = lookup_constant cst env in
match cb.Declarations.const_proj with
- | Some {Declarations.proj_ind = mind; proj_npars = n; proj_arg = m; proj_type = ty} ->
+ | Some {Declarations.proj_ind = mind; proj_npars = n;
+ proj_arg = m; proj_type = ty} ->
(cst,mind,n,m,ty)
| None -> raise Not_found
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 86bc44a62..9f2a00135 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -20,14 +20,15 @@ let get_current_proof_name = Proof_global.get_current_proof_name
let get_all_proof_names = Proof_global.get_all_proof_names
type lemma_possible_guards = Proof_global.lemma_possible_guards
+type universe_binders = Proof_global.universe_binders
let delete_proof = Proof_global.discard
let delete_current_proof = Proof_global.discard_current
let delete_all_proofs = Proof_global.discard_all
-let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator =
+let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
let goals = [ (Global.env_of_context hyps , c) ] in
- Proof_global.start_proof sigma id str goals terminator;
+ Proof_global.start_proof sigma id ?pl str goals terminator;
let env = Global.env () in
ignore (Proof_global.with_current_proof (fun _ p ->
match init_tac with
@@ -54,6 +55,9 @@ let set_used_variables l =
let get_used_variables () =
Proof_global.get_used_variables ()
+let get_universe_binders () =
+ Proof_global.get_universe_binders ()
+
exception NoSuchGoal
let _ = Errors.register_handler begin function
| NoSuchGoal -> Errors.error "No such goal."
@@ -140,7 +144,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
let status = by tac in
let _,(const,univs,_) = cook_proof () in
delete_current_proof ();
- const, status, univs
+ const, status, fst univs
with reraise ->
let reraise = Errors.push reraise in
delete_current_proof ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index fc521ea43..d0528c9fd 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -55,8 +55,10 @@ val delete_all_proofs : unit -> unit
type lemma_possible_guards = Proof_global.lemma_possible_guards
+type universe_binders = Id.t Loc.located list
+
val start_proof :
- Id.t -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
+ Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
?init_tac:unit Proofview.tactic ->
Proof_global.proof_terminator -> unit
@@ -121,6 +123,9 @@ val set_used_variables :
Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
val get_used_variables : unit -> Context.section_context option
+(** {6 Universe binders } *)
+val get_universe_binders : unit -> universe_binders option
+
(** {6 ... } *)
(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
subgoal of the current focused proof or raises a [UserError] if no
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 1e0de05dd..31706b3d0 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -63,14 +63,14 @@ let _ =
(* Extra info on proofs. *)
type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context
+type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type universe_binders = Id.t Loc.located list
type proof_object = {
id : Names.Id.t;
entries : Safe_typing.private_constants Entries.definition_entry list;
persistence : Decl_kinds.goal_kind;
universes: proof_universes;
- (* constraints : Univ.constraints; *)
}
type proof_ending =
@@ -89,6 +89,7 @@ type pstate = {
proof : Proof.proof;
strength : Decl_kinds.goal_kind;
mode : proof_mode Ephemeron.key;
+ universe_binders: universe_binders option;
}
let make_terminator f = f
@@ -229,7 +230,7 @@ let disactivate_proof_mode mode =
end of the proof to close the proof. The proof is started in the
evar map [sigma] (which can typically contain universe
constraints). *)
-let start_proof sigma id str goals terminator =
+let start_proof sigma id ?pl str goals terminator =
let initial_state = {
pid = id;
terminator = Ephemeron.create terminator;
@@ -237,10 +238,11 @@ let start_proof sigma id str goals terminator =
endline_tactic = None;
section_vars = None;
strength = str;
- mode = find_proof_mode "No" } in
+ mode = find_proof_mode "No";
+ universe_binders = pl } in
push initial_state pstates
-let start_dependent_proof id str goals terminator =
+let start_dependent_proof id ?pl str goals terminator =
let initial_state = {
pid = id;
terminator = Ephemeron.create terminator;
@@ -248,10 +250,12 @@ let start_dependent_proof id str goals terminator =
endline_tactic = None;
section_vars = None;
strength = str;
- mode = find_proof_mode "No" } in
+ mode = find_proof_mode "No";
+ universe_binders = pl } in
push initial_state pstates
let get_used_variables () = (cur_pstate ()).section_vars
+let get_universe_binders () = (cur_pstate ()).universe_binders
let proof_using_auto_clear = ref true
let _ = Goptions.declare_bool_option
@@ -304,7 +308,8 @@ let constrain_variables init uctx =
Univ.ContextSet.add_constraints cstrs (UState.context_set uctx)
let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
- let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
+ let { pid; section_vars; strength; proof; terminator; universe_binders } =
+ cur_pstate () in
let poly = pi2 strength (* Polymorphic *) in
let initial_goals = Proof.initial_goals proof in
let initial_euctx = Proof.initial_euctx proof in
@@ -370,8 +375,13 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
const_entry_opaque = true;
const_entry_universes = univs;
const_entry_polymorphic = poly})
- fpl initial_goals in
- { id = pid; entries = entries; persistence = strength; universes = universes },
+ fpl initial_goals in
+ let binders =
+ Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
+ universe_binders
+ in
+ { id = pid; entries = entries; persistence = strength;
+ universes = (universes, binders) },
fun pr_ending -> Ephemeron.get terminator pr_ending
type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 3fbcefd0a..5f1158950 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -55,18 +55,18 @@ val compact_the_proof : unit -> unit
(i.e. an proof ending command) and registers the appropriate
values. *)
type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context
+type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type universe_binders = Names.Id.t Loc.located list
type proof_object = {
id : Names.Id.t;
entries : Safe_typing.private_constants Entries.definition_entry list;
persistence : Decl_kinds.goal_kind;
universes: proof_universes;
- (* constraints : Univ.constraints; *)
- (** guards : lemma_possible_guards; *)
}
type proof_ending =
- | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
+ | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
+ proof_universes
| Proved of Vernacexpr.opacity_flag *
(Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
proof_object
@@ -83,14 +83,15 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
closing commands and the xml plugin); [terminator] is used at the
end of the proof to close the proof. *)
val start_proof :
- Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list ->
+ Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
+ Decl_kinds.goal_kind -> (Environ.env * Term.types) list ->
proof_terminator -> unit
(** Like [start_proof] except that there may be dependencies between
initial goals. *)
val start_dependent_proof :
- Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope ->
- proof_terminator -> unit
+ Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind ->
+ Proofview.telescope -> proof_terminator -> unit
(** Update the proofs global environment after a side-effecting command
(e.g. a sublemma definition) has been run inside it. Assumes
@@ -143,6 +144,8 @@ val set_used_variables :
Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
val get_used_variables : unit -> Context.section_context option
+val get_universe_binders : unit -> universe_binders option
+
(**********************************************************)
(* *)
(* Proof modes *)
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 17a10ccba..0a542c9c0 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -186,7 +186,7 @@ let look_for_possibly_mutual_statements = function
(* Saving a goal *)
-let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
try
let const = adjust_guardness_conditions const do_guard in
@@ -205,6 +205,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
(locality, ConstRef kn) in
definition_message id;
+ Option.iter (Universes.register_universe_binders r) pl;
call_hook (fun exn -> exn) hook l r
with e when Errors.noncritical e ->
let e = Errors.push e in
@@ -219,11 +220,11 @@ let compute_proof_name locality = function
locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
then
user_err_loc (loc,"",pr_id id ++ str " already exists.");
- id
+ id, pl
| None ->
- next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ())
+ next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
let t_i = norm t_i in
match body with
| None ->
@@ -276,28 +277,28 @@ let save_hook = ref ignore
let set_save_hook f = save_hook := f
let save_named ?export_seff proof =
- let id,const,cstrs,do_guard,persistence,hook = proof in
- save ?export_seff id const cstrs do_guard persistence hook
+ let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+ save ?export_seff id const cstrs pl do_guard persistence hook
let check_anonymity id save_ident =
if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
error "This command can only be used for unnamed theorem."
-
let save_anonymous ?export_seff proof save_ident =
- let id,const,cstrs,do_guard,persistence,hook = proof in
+ let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
check_anonymity id save_ident;
- save ?export_seff save_ident const cstrs do_guard persistence hook
+ save ?export_seff save_ident const cstrs pl do_guard persistence hook
let save_anonymous_with_strength ?export_seff proof kind save_ident =
- let id,const,cstrs,do_guard,_,hook = proof in
+ let id,const,(cstrs,pl),do_guard,_,hook = proof in
check_anonymity id save_ident;
(* we consider that non opaque behaves as local for discharge *)
- save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+ save ?export_seff save_ident const cstrs pl do_guard
+ (Global, const.const_entry_polymorphic, Proof kind) hook
(* Admitted *)
-let admit (id,k,e) hook () =
+let admit (id,k,e) pl hook () =
let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
let () = match k with
| Global, _, _ -> ()
@@ -306,6 +307,7 @@ let admit (id,k,e) hook () =
str "declared as an axiom.")
in
let () = assumption_message id in
+ Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
call_hook (fun exn -> exn) hook Global (ConstRef kn)
(* Starting a goal *)
@@ -315,11 +317,10 @@ let set_start_hook = (:=) start_hook
let get_proof proof do_guard hook opacity =
- let (id,(const,cstrs,persistence)) =
+ let (id,(const,univs,persistence)) =
Pfedit.cook_this_proof proof
in
- (** FIXME *)
- id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook
+ id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
let check_exist =
List.iter (fun (loc,id) ->
@@ -330,16 +331,16 @@ let check_exist =
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
- | Admitted (id,k,pe,ctx) ->
- admit (id,k,pe) (hook (Some ctx)) ();
+ | Admitted (id,k,pe,(ctx,pl)) ->
+ admit (id,k,pe) pl (hook (Some ctx)) ();
Pp.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff, exports = match opaque with
| Vernacexpr.Transparent -> false, true, []
| Vernacexpr.Opaque None -> true, false, []
| Vernacexpr.Opaque (Some l) -> true, true, l in
- let proof = get_proof proof compute_guard
- (hook (Some proof.Proof_global.universes)) is_opaque in
+ let proof = get_proof proof compute_guard
+ (hook (Some (fst proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
| Some ((_,id),None) -> save_anonymous ~export_seff proof id
@@ -352,7 +353,7 @@ let universe_proof_terminator compute_guard hook =
let standard_proof_terminator compute_guard hook =
universe_proof_terminator compute_guard (fun _ -> hook)
-let start_proof id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
let terminator = match terminator with
| None -> standard_proof_terminator compute_guard hook
| Some terminator -> terminator compute_guard hook
@@ -363,9 +364,9 @@ let start_proof id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[])
| None -> initialize_named_context_for_proof ()
in
!start_hook c;
- Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+ Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
-let start_proof_univs id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
let terminator = match terminator with
| None -> universe_proof_terminator compute_guard hook
| Some terminator -> terminator compute_guard hook
@@ -376,11 +377,11 @@ let start_proof_univs id kind sigma ?terminator ?sign c ?init_tac ?(compute_guar
| None -> initialize_named_context_for_proof ()
in
!start_hook c;
- Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+ Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
let rec_tac_initializer finite guard thms snl =
if finite then
- match List.map (fun (id,(t,_)) -> (id,t)) thms with
+ match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
| (id,_)::l -> Tactics.mutual_cofix id l 0
| _ -> assert false
else
@@ -388,7 +389,7 @@ let rec_tac_initializer finite guard thms snl =
let nl = match snl with
| None -> List.map succ (List.map List.last guard)
| Some nl -> nl
- in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+ in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
@@ -417,7 +418,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
(if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
match thms with
| [] -> anomaly (Pp.str "No proof to start")
- | (id,(t,(_,imps)))::other_thms ->
+ | ((id,pl),(t,(_,imps)))::other_thms ->
let hook ctx strength ref =
let ctx = match ctx with
| None -> Evd.empty_evar_universe_context
@@ -436,7 +437,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
call_hook (fun exn -> exn) hook strength ref) thms_data in
- start_proof_univs id kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+ start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
let start_proof_com kind thms hook =
let env0 = Global.env () in
@@ -480,14 +481,13 @@ let save_proof ?proof = function
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
+ let ctx = Evd.evar_context_universe_context (fst universes) in
Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
| None ->
let id, k, typ = Pfedit.current_proof_statement () in
(* This will warn if the proof is complete *)
let pproofs, universes =
Proof_global.return_proof ~allow_partial:true () in
- let ctx = Evd.evar_context_universe_context universes in
let sec_vars =
match Pfedit.get_used_variables(), pproofs with
| Some _ as x, _ -> x
@@ -497,7 +497,10 @@ let save_proof ?proof = function
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),universes)
+ let names = Pfedit.get_universe_binders () in
+ let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in
+ Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
+ (universes, Some binders))
in
Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
| Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index dca6afe19..e2ddf79df 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -14,7 +14,6 @@ open Vernacexpr
open Pfedit
type 'a declaration_hook
-
val mk_hook :
(Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
@@ -24,29 +23,31 @@ val call_hook :
(** A hook start_proof calls on the type of the definition being started *)
val set_start_hook : (types -> unit) -> unit
-val start_proof : Id.t -> goal_kind -> Evd.evar_map ->
+val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
unit declaration_hook -> unit
-val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map ->
- ?terminator:(lemma_possible_guards -> (Proof_global.proof_universes option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+ ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
- (Proof_global.proof_universes option -> unit declaration_hook) -> unit
+ (Evd.evar_universe_context option -> unit declaration_hook) -> unit
val start_proof_com : goal_kind -> Vernacexpr.proof_expr list ->
unit declaration_hook -> unit
val start_proof_with_initialization :
- goal_kind -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
- (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
+ goal_kind -> Evd.evar_map ->
+ (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
+ ((Id.t * universe_binders option) *
+ (types * (Name.t list * Impargs.manual_explicitation list))) list
-> int list option -> unit declaration_hook -> unit
val universe_proof_terminator :
Proof_global.lemma_possible_guards ->
- (Proof_global.proof_universes option -> unit declaration_hook) ->
+ (Evd.evar_universe_context option -> unit declaration_hook) ->
Proof_global.proof_terminator
val standard_proof_terminator :
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 5201d54d6..bf8f34855 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -266,7 +266,7 @@ TACTIC EXTEND rewrite_star
let add_rewrite_hint bases ort t lcsr =
let env = Global.env() in
let sigma = Evd.from_env env in
- let poly = Flags.is_universe_polymorphism () in
+ let poly = Flags.use_polymorphic_flag () in
let f ce =
let c, ctx = Constrintern.interp_constr env sigma ce in
let ctx =
diff --git a/test-suite/bugs/closed/3735.v b/test-suite/bugs/closed/3735.v
new file mode 100644
index 000000000..a50572ace
--- /dev/null
+++ b/test-suite/bugs/closed/3735.v
@@ -0,0 +1,4 @@
+Require Import Coq.Program.Tactics.
+Class Foo := { bar : Type }.
+Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *)
+Fail Program Lemma foo : Foo -> bar. \ No newline at end of file
diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v
new file mode 100644
index 000000000..108ebf592
--- /dev/null
+++ b/test-suite/bugs/closed/3807.v
@@ -0,0 +1,33 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Unset Universe Minimization ToSet.
+
+
+Definition foo : Type := nat.
+About foo.
+(* foo@{Top.1} : Type@{Top.1}*)
+(* Top.1 |= *)
+
+Definition bar : foo -> nat.
+Admitted.
+About bar.
+(* bar@{Top.2} : foo@{Top.2} -> nat *)
+(* Top.2 |= *)
+
+Lemma baz@{i} : foo@{i} -> nat.
+Proof.
+ exact bar.
+Defined.
+
+Definition bar'@{i} : foo@{i} -> nat.
+ intros f. exact 0.
+Admitted.
+About bar'.
+(* bar'@{i} : foo@{i} -> nat *)
+(* i |= *)
+
+Axiom f@{i} : Type@{i}.
+(*
+*** [ f@{i} : Type@{i} ]
+(* i |= *)
+*) \ No newline at end of file
diff --git a/test-suite/bugs/closed/4284.v b/test-suite/bugs/closed/4284.v
new file mode 100644
index 000000000..0fff3026f
--- /dev/null
+++ b/test-suite/bugs/closed/4284.v
@@ -0,0 +1,6 @@
+Set Primitive Projections.
+Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }.
+Theorem onefiber' {X : Type} (P : X -> Type) (x : X) : True.
+Proof.
+set (Q1 := total2 (fun f => pr1 P f = x)).
+set (f1:=fun q1 : Q1 => pr2 _ (pr1 _ q1)).
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index 0623cf5b8..43c9b5129 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -118,8 +118,6 @@ Definition setle (B : Type@{i}) :=
let foo (A : Type@{j}) := A in foo B.
Fail Check @setlt@{j Prop}.
-Check @setlt@{Prop j}.
-Check @setle@{Prop j}.
-
Fail Definition foo := @setle@{j Prop}.
-Definition foo := @setle@{Prop j}.
+Check setlt@{Set i}.
+Check setlt@{Set j}. \ No newline at end of file
diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
new file mode 100644
index 000000000..5c23f8404
--- /dev/null
+++ b/test-suite/bugs/closed/4400.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
+Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
+Set Printing Universes.
+Inductive Foo (I : Type -> Type) (A : Type) : Type :=
+| foo (B : Type) : A -> I B -> Foo I A.
+Definition Family := Type -> Type.
+Definition FooToo : Family -> Family := Foo.
+Definition optionize (I : Type -> Type) (A : Type) := option (I A).
+Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A.
+Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
+Definition barRec : Rec (optionize id) := {| rec := bar id |}.
+Inductive Empty {T} : T -> Prop := .
+Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family)
+nil)) (b : unit) :
+ Empty (a, b) -> False.
+Proof.
+ intro e.
+ dependent induction e.
+Qed.
diff --git a/test-suite/bugs/closed/4433.v b/test-suite/bugs/closed/4433.v
new file mode 100644
index 000000000..9eeb86468
--- /dev/null
+++ b/test-suite/bugs/closed/4433.v
@@ -0,0 +1,29 @@
+Require Import Coq.Arith.Arith Coq.Init.Wf.
+Axiom proof_admitted : False.
+Goal exists x y z : nat, Fix
+ Wf_nat.lt_wf
+ (fun _ => nat -> nat)
+ (fun x' f => match x' as x'0
+ return match x'0 with
+ | 0 => True
+ | S x'' => x'' < x'
+ end
+ -> nat -> nat
+ with
+ | 0 => fun _ _ => 0
+ | S x'' => f x''
+ end
+ (match x' with
+ | 0 => I
+ | S x'' => (Nat.lt_succ_diag_r _)
+ end))
+ z
+ y
+ = 0.
+Proof.
+ do 3 (eexists; [ shelve.. | ]).
+ match goal with |- ?G => let G' := (eval lazy in G) in change G with G' end.
+ case proof_admitted.
+ Unshelve.
+ all:constructor.
+Defined. \ No newline at end of file
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2371d32cd..b72a06740 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -101,3 +101,9 @@ Fail Check fun x => match x with S (FORALL x, _) => 0 end.
Parameter traverse : (nat -> unit) -> (nat -> unit).
Notation traverse_var f l := (traverse (fun l => f l) l).
+
+(* Check that when an ident become a keyword, it does not break
+ previous rules relying on the string to be classified as an ident *)
+
+Notation "'intros' x" := (S x) (at level 0).
+Goal True -> True. intros H. exact H. Qed.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index fdedbf672..b13671cec 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -269,16 +269,6 @@ Section GenericInstances.
Unset Strict Universe Declaration.
(** The complement of a crelation conserves its proper elements. *)
- Program Definition complement_proper (A : Type@{k}) (RA : crelation A)
- `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
- Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _.
-
- Next Obligation.
- Proof.
- unfold complement.
- pose (mR x y X x0 y0 X0).
- intuition.
- Qed.
(** The [flip] too, actually the [flip] instance is a bit more general. *)
Program Definition flip_proper
@@ -521,8 +511,8 @@ Ltac proper_reflexive :=
Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
-Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper
- : typeclass_instances.
+(* Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper *)
+(* : typeclass_instances. *)
Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper
: typeclass_instances.
Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 6f736e45f..cdc3e0461 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -658,4 +658,3 @@ Proof.
exists x; intro; exact Hx.
exists x0; exact Hnot.
Qed.
-
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index ede51f57f..4e582934a 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -344,53 +344,6 @@ End Paradox.
End NoRetractToImpredicativeUniverse.
-(** * Prop is not a retract *)
-
-(** The existence in the pure Calculus of Constructions of a retract
- from [Prop] into a small type of [Prop] is inconsistent. This is a
- special case of the previous result. *)
-
-Module NoRetractFromSmallPropositionToProp.
-
-Section Paradox.
-
-(** ** Retract of [Prop] in a small type *)
-
-(** The retract is axiomatized using logical equivalence as the
- equality on propositions. *)
-
-Variable bool : Prop.
-Variable p2b : Prop -> bool.
-Variable b2p : bool -> Prop.
-Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
-Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
-
-(** ** Paradox *)
-
-Theorem paradox : forall B:Prop, B.
-Proof.
- intros B.
- pose proof
- (NoRetractToImpredicativeUniverse.paradox@{Type Prop}) as P.
- refine (P _ _ _ _ _ _ _ _ _ _);clear P.
- + exact bool.
- + exact (fun x => forall P:Prop, (x->P)->P).
- + cbn. exact (fun _ x P k => k x).
- + cbn. intros F P x.
- apply P.
- intros f.
- exact (f x).
- + cbn. easy.
- + exact b2p.
- + exact p2b.
- + exact p2p2.
- + exact p2p1.
-Qed.
-
-End Paradox.
-
-End NoRetractFromSmallPropositionToProp.
-
(** * Modal fragments of [Prop] are not retracts *)
(** In presence of a a monadic modality on [Prop], we can define a
@@ -534,6 +487,80 @@ End Paradox.
End NoRetractToNegativeProp.
+(** * Prop is not a retract *)
+
+(** The existence in the pure Calculus of Constructions of a retract
+ from [Prop] into a small type of [Prop] is inconsistent. This is a
+ special case of the previous result. *)
+
+Module NoRetractFromSmallPropositionToProp.
+
+(** ** The universe of propositions. *)
+
+Definition NProp := { P:Prop | P -> P}.
+Definition El : NProp -> Prop := @proj1_sig _ _.
+
+Section MParadox.
+
+(** ** Retract of [Prop] in a small type, using the identity modality. *)
+
+Variable bool : NProp.
+Variable p2b : NProp -> El bool.
+Variable b2p : El bool -> NProp.
+Hypothesis p2p1 : forall A:NProp, El (b2p (p2b A)) -> El A.
+Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
+
+(** ** Paradox *)
+
+Theorem mparadox : forall B:NProp, El B.
+Proof.
+ intros B.
+ refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+ + exact (fun P => P).
+ + cbn. auto.
+ + cbn. auto.
+ + cbn. auto.
+ + exact bool.
+ + exact p2b.
+ + exact b2p.
+ + auto.
+ + auto.
+ + exact B.
+ + exact h.
+Qed.
+
+End MParadox.
+
+Section Paradox.
+
+(** ** Retract of [Prop] in a small type *)
+
+(** The retract is axiomatized using logical equivalence as the
+ equality on propositions. *)
+Variable bool : Prop.
+Variable p2b : Prop -> bool.
+Variable b2p : bool -> Prop.
+Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
+Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
+
+(** ** Paradox *)
+
+Theorem paradox : forall B:Prop, B.
+Proof.
+ intros B.
+ refine (mparadox (exist _ bool (fun x => x)) _ _ _ _
+ (exist _ B (fun x => x))).
+ + intros p. red. red. exact (p2b (El p)).
+ + cbn. intros b. red. exists (b2p b). exact (fun x => x).
+ + cbn. intros [A H]. cbn. apply p2p1.
+ + cbn. intros [A H]. cbn. apply p2p2.
+Qed.
+
+End Paradox.
+
+End NoRetractFromSmallPropositionToProp.
+
+
(** * Large universes are no retracts of [Prop]. *)
(** The existence in the Calculus of Constructions with universes of a
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0b709a3fc..91cfddb54 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1128,7 +1128,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+ List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+ fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
@@ -1164,7 +1165,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+ List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+ fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index e34cbab5f..50ecef0b0 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -826,10 +826,10 @@ let obligation_terminator name num guard hook pf =
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 prg = { prg with prg_ctx = fst uctx } in
let obls, rem = prg.prg_obligations in
let obl = obls.(num) in
- let ctx = Evd.evar_context_universe_context uctx in
+ let ctx = Evd.evar_context_universe_context (fst uctx) in
let (_, obl) = declare_obligation prg obl body ty ctx in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b6a4ab93e..b3512ffde 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -2048,7 +2048,7 @@ let check_vernac_supports_polymorphism c p =
let enforce_polymorphism = function
| None -> Flags.is_universe_polymorphism ()
- | Some b -> b
+ | Some b -> Flags.make_polymorphic_flag b; b
(** A global default timeout, controled by option "Set Default Timeout n".
Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2149,7 +2149,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
then Flags.verbosely (interp ?proof ~loc locality poly) c
else Flags.silently (interp ?proof ~loc locality poly) c;
if orig_program_mode || not !Flags.program_mode || isprogcmd then
- Flags.program_mode := orig_program_mode
+ Flags.program_mode := orig_program_mode;
+ ignore (Flags.use_polymorphic_flag ())
end
with
| reraise when
@@ -2161,6 +2162,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
let e = locate_if_not_already loc e in
let () = restore_timeout () in
Flags.program_mode := orig_program_mode;
+ ignore (Flags.use_polymorphic_flag ());
iraise e
and aux_list ?locality ?polymorphism isprogcmd l =
List.iter (aux false) (List.map snd l)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 07:10:13 +0000