diff options
42 files changed, 131 insertions, 272 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 8c52655ff..02330339d 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -143,6 +143,6 @@ let cook_constant env r = let t = mkArity (ctx,Type s.poly_level) in let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in let j = make_judge (constr_of_def body) typ in - Typeops.make_polymorphic env j + Typeops.make_polymorphic_if_constant_for_ind env j in (body, typ, cb.const_constraints) diff --git a/kernel/entries.ml b/kernel/entries.ml index 32dfaae8f..28f11c9af 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -55,10 +55,9 @@ type mutual_inductive_entry = { (*s Constants (Definition/Axiom) *) type definition_entry = { - const_entry_body : constr; - const_entry_type : types option; - const_entry_polymorphic : bool; - const_entry_opaque : bool } + const_entry_body : constr; + const_entry_type : types option; + const_entry_opaque : bool } type inline = int option (* inlining level, None for no inlining *) diff --git a/kernel/entries.mli b/kernel/entries.mli index 5d9569de4..08740afae 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -51,10 +51,9 @@ type mutual_inductive_entry = { (** {6 Constants (Definition/Axiom) } *) type definition_entry = { - const_entry_body : constr; - const_entry_type : types option; - const_entry_polymorphic : bool; - const_entry_opaque : bool } + const_entry_body : constr; + const_entry_type : types option; + const_entry_opaque : bool } type inline = int option (* inlining level, None for no inlining *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 97d2fe521..6b44bcad3 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -26,8 +26,9 @@ open Type_errors open Indtypes open Typeops -let constrain_type env j cst1 poly = function - | None -> make_polymorphic env j, cst1 +let constrain_type env j cst1 = function + | None -> + make_polymorphic_if_constant_for_ind env j, cst1 | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in @@ -92,9 +93,7 @@ let infer_declaration env dcl = match dcl with | DefinitionEntry c -> let (j,cst) = infer env c.const_entry_body in - let (typ,cst) = constrain_type env j cst - c.const_entry_polymorphic c.const_entry_type - in + let (typ,cst) = constrain_type env j cst c.const_entry_type in let def = if c.const_entry_opaque then OpaqueDef (Declarations.opaque_from_val j.uj_val) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b7a8b7d4e..85e8e6c88 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -130,10 +130,10 @@ let extract_context_levels env = List.fold_left (fun l (_,b,p) -> if b=None then extract_level env p::l else l) [] -let make_polymorphic env {uj_val = c; uj_type = t} = +let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = let params, ccl = dest_prod_assum env t in match kind_of_term ccl with - | Sort (Type u) -> + | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> let param_ccls = extract_context_levels env params in let s = { poly_param_levels = param_ccls; poly_level = u} in PolymorphicArity (params,s) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index af46b9875..c1c805f38 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -101,5 +101,6 @@ val type_of_constant_knowing_parameters : env -> constant_type -> constr array -> types (** Make a type polymorphic if an arity *) -val make_polymorphic : env -> unsafe_judgment -> constant_type +val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> + constant_type diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index bdc855869..ba40f98c0 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -15,8 +15,6 @@ type locality = | Local | Global -type polymorphic = bool - type theorem_kind = | Theorem | Lemma @@ -50,9 +48,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * polymorphic * assumption_object_kind +type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * polymorphic * definition_object_kind +type definition_kind = locality * definition_object_kind (* Kinds used in proofs *) @@ -60,7 +58,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * polymorphic * goal_object_kind +type goal_kind = locality * goal_object_kind (* Kinds used in library *) @@ -84,23 +82,22 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -let string_of_definition_kind (gl,p,k) = - let s = match gl, k with - | Local, Coercion -> "Coercion Local" - | Global, Coercion -> "Coercion" - | Local, Definition -> "Let" - | Global, Definition -> "Definition" - | Local, SubClass -> "Local SubClass" - | Global, SubClass -> "SubClass" - | Global, CanonicalStructure -> "Canonical Structure" - | Global, Example -> "Example" - | Local, (CanonicalStructure|Example) -> - anomaly "Unsupported local definition kind" - | Local, Instance -> "Instance" - | Global, Instance -> "Global Instance" - | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) - -> anomaly "Internal definition kind" - in if p then "Polymorphic " ^ s else s +let string_of_definition_kind def = + match def with + | Local, Coercion -> "Coercion Local" + | Global, Coercion -> "Coercion" + | Local, Definition -> "Let" + | Global, Definition -> "Definition" + | Local, SubClass -> "Local SubClass" + | Global, SubClass -> "SubClass" + | Global, CanonicalStructure -> "Canonical Structure" + | Global, Example -> "Example" + | Local, (CanonicalStructure|Example) -> + anomaly "Unsupported local definition kind" + | Local, Instance -> "Instance" + | Global, Instance -> "Global Instance" + | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) + -> anomaly "Internal definition kind" (* Strength *) diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 1e4ad07e8..88ef763c9 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -15,8 +15,6 @@ type locality = | Local | Global -type polymorphic = bool - type theorem_kind = | Theorem | Lemma @@ -50,9 +48,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * polymorphic * assumption_object_kind +type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * polymorphic * definition_object_kind +type definition_kind = locality * definition_object_kind (** Kinds used in proofs *) @@ -60,7 +58,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * polymorphic * goal_object_kind +type goal_kind = locality * goal_object_kind (** Kinds used in library *) @@ -74,7 +72,7 @@ type logical_kind = val logical_kind_of_goal_kind : goal_object_kind -> logical_kind val string_of_theorem_kind : theorem_kind -> string val string_of_definition_kind : - locality * polymorphic * definition_object_kind -> string + locality * definition_object_kind -> string (** About locality *) diff --git a/library/declare.ml b/library/declare.ml index ec713d5b2..c566cedfd 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -160,8 +160,7 @@ let hcons_constant_declaration = function DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; const_entry_type = Option.map hcons1_constr ce.const_entry_type; - const_entry_polymorphic = ce.const_entry_polymorphic; - const_entry_opaque = ce.const_entry_opaque } + const_entry_opaque = ce.const_entry_opaque } | cd -> cd let declare_constant_common id dhyps (cd,kind) = diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 73c3ca8c0..160d94130 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -135,36 +135,25 @@ let test_plurial_form_types = function "Keywords Implicit Types expect more than one type" | _ -> () -let polymorphic_flag = ref None -let use_polymorphic_flag () = - let fl = match !polymorphic_flag with Some p -> p | None -> assert false in - polymorphic_flag := None; fl - (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion typeclass_constraint record_field decl_notation rec_definition; gallina: - [ [ [ "Polymorphic" -> polymorphic_flag := Some true | -> polymorphic_flag := Some false ]; - g = gallina_def -> g ] ] - ; - - gallina_def: (* Definition, Theorem, Variable, Axiom, ... *) [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr; l = LIST0 [ "with"; id = identref; bl = binders; ":"; c = lconstr -> (Some id,(bl,c,None)) ] -> - VernacStartTheoremProof (thm,use_polymorphic_flag (),(Some id,(bl,c,None))::l, false, no_hook) - | (g, k) = assumption_token; nl = inline; bl = assum_list -> - VernacAssumption ((g, use_polymorphic_flag (), k), nl, bl) - | (g, k) = assumptions_token; nl = inline; bl = assum_list -> + VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook) + | stre = assumption_token; nl = inline; bl = assum_list -> + VernacAssumption (stre, nl, bl) + | stre = assumptions_token; nl = inline; bl = assum_list -> test_plurial_form bl; - VernacAssumption ((g, use_polymorphic_flag (), k), nl, bl) - | (f,(g,k)) = def_token; id = identref; - b = def_body -> - VernacDefinition ((g,use_polymorphic_flag (),k), id, b, f) + VernacAssumption (stre, nl, bl) + | (f,d) = def_token; id = identref; b = def_body -> + VernacDefinition (d, id, b, f) (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> @@ -531,16 +520,16 @@ GEXTEND Gram d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition - ((Global,false,CanonicalStructure),(dummy_loc,s),d, + ((Global,CanonicalStructure),(dummy_loc,s),d, (fun _ -> Recordops.declare_canonical_structure)) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((use_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((use_locality_exp (),Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((enforce_locality_exp true,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((enforce_locality_exp true,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (enforce_locality_exp true, f, s, t) @@ -568,7 +557,7 @@ GEXTEND Gram pri = OPT [ "|"; i = natural -> i ] ; props = [ ":="; "{"; r = record_declaration; "}" -> Some r | ":="; c = lconstr -> Some c | -> None ] -> - VernacInstance (false, not (use_section_locality ()), false, + VernacInstance (false, not (use_section_locality ()), snd namesup, (fst namesup, expl, t), props, pri) | IDENT "Existing"; IDENT "Instance"; id = global -> @@ -639,7 +628,7 @@ GEXTEND Gram | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] -> - VernacInstance (true, not (use_section_locality ()), false, + VernacInstance (true, not (use_section_locality ()), snd namesup, (fst namesup, expl, t), None, pri) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index d21b83ab6..4bf6e59f1 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -347,20 +347,18 @@ let pr_class_rawexpr = function | SortClass -> str"Sortclass" | RefClass qid -> pr_smart_global qid -let pr_assumption_token many (l,p,k) = - let s = match l, k with - | (Local,Logical) -> - str (if many then "Hypotheses" else "Hypothesis") - | (Local,Definitional) -> - str (if many then "Variables" else "Variable") - | (Global,Logical) -> - str (if many then "Axioms" else "Axiom") - | (Global,Definitional) -> - str (if many then "Parameters" else "Parameter") - | (Global,Conjectural) -> str"Conjecture" - | (Local,Conjectural) -> - anomaly "Don't know how to beautify a local conjecture" - in if p then str "Polymorphic " ++ s else s +let pr_assumption_token many = function + | (Local,Logical) -> + str (if many then "Hypotheses" else "Hypothesis") + | (Local,Definitional) -> + str (if many then "Variables" else "Variable") + | (Global,Logical) -> + str (if many then "Axioms" else "Axiom") + | (Global,Definitional) -> + str (if many then "Parameters" else "Parameter") + | (Global,Conjectural) -> str"Conjecture" + | (Local,Conjectural) -> + anomaly "Don't know how to beautify a local conjecture" let pr_params pr_c (xl,(c,t)) = hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ @@ -571,7 +569,7 @@ let rec pr_vernac = function | None -> mt() | Some cc -> str" :=" ++ spc() ++ cc)) - | VernacStartTheoremProof (ki,p,l,_,_) -> + | VernacStartTheoremProof (ki,l,_,_) -> hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ prlist (pr_statement (spc () ++ str "with")) (List.tl l)) @@ -692,11 +690,10 @@ let rec pr_vernac = function (* prlist_with_sep (fun () -> str";" ++ spc()) *) (* (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) *) - | VernacInstance (abst,glob,poly,sup,(instid, bk, cl),props,pri) -> + | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) -> hov 1 ( pr_non_locality (not glob) ++ (if abst then str"Declare " else mt ()) ++ - (if poly then str"Polymorphic " else mt ()) ++ str"Instance" ++ spc () ++ pr_and_type_binders_arg sup ++ str"=>" ++ spc () ++ diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c1b3c0b84..4f32bbd99 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -973,7 +973,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = Ensures by: obvious i*) (mk_equation_id f_id) - (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) lemma_type (fun _ _ -> ()); Pfedit.by (prove_replacement); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d3949731b..2ba29ced7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -333,7 +333,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro begin Lemmas.start_proof new_princ_name - (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) new_principle_type (hook new_principle_type) ; @@ -382,7 +382,6 @@ let generate_functional_principle let ce = { const_entry_body = value; const_entry_type = None; - const_entry_polymorphic = false; const_entry_opaque = false } in ignore( diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0e4dd1289..dd48765fb 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -351,9 +351,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in let ce,imps = - Command.interp_definition bl false None body (Some ret_type) + Command.interp_definition bl None body (Some ret_type) in - Command.declare_definition + Command.declare_definition fname (Decl_kinds.Global,Decl_kinds.Definition) ce imps (fun _ _ -> ()) | _ -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a0d2061bc..094d2e50f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -156,7 +156,7 @@ let definition_message id = Flags.if_verbose message ((string_of_id id) ^ " is defined") -let save with_clean id const (locality,p,kind) hook = +let save with_clean id const (locality,kind) hook = let {const_entry_body = pft; const_entry_type = tpo; const_entry_opaque = opacity } = const in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ce484ca23..426b496dd 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -788,7 +788,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Ensures by: obvious i*) (mk_correct_id f_id) - (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i)); @@ -840,7 +840,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Ensures by: obvious i*) (mk_complete_id f_id) - (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i)); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 24379e7b4..11fbc01ba 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1021,7 +1021,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ in start_proof na - (Decl_kinds.Global, false, Decl_kinds.Proof Decl_kinds.Lemma) + (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) sign gls_type hook ; @@ -1071,7 +1071,7 @@ let com_terminate let start_proof (tac_start:tactic) (tac_end:tactic) = let (evmap, env) = Lemmas.get_current_context() in start_proof thm_name - (Global, false, Proof Lemma) (Environ.named_context_val env) + (Global, Proof Lemma) (Environ.named_context_val env) (hyp_terminates nb_args fonctional_ref) hook; by (observe_tac "starting_tac" tac_start); @@ -1140,7 +1140,6 @@ let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = fun f_id kind value -> let ce = {const_entry_body = value; const_entry_type = None; - const_entry_polymorphic = false; const_entry_opaque = false } in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; @@ -1350,7 +1349,7 @@ let (com_eqn : int -> identifier -> let (evmap, env) = Lemmas.get_current_context() in let f_constr = (constr_of_global f_ref) in let equation_lemma_type = subst1 f_constr equation_lemma_type in - (start_proof eq_name (Global, false, Proof Lemma) + (start_proof eq_name (Global, Proof Lemma) (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); by (start_equation f_ref terminate_ref diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index d434a890f..38c65cdd0 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -159,7 +159,6 @@ let decl_constant na c = mkConst(declare_constant (id_of_string na) (DefinitionEntry { const_entry_body = c; const_entry_type = None; - const_entry_polymorphic = false; const_entry_opaque = true }, IsProof Lemma)) diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 7faf78033..fbdaa8d3b 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -113,7 +113,7 @@ let dump_constraint ty ((loc, n), _, _) = let dump_variable lid = () let vernac_assumption env isevars kind l nl = - let global = pi1 kind = Global in + let global = fst kind = Global in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun lid -> @@ -137,8 +137,7 @@ let subtac (loc, command) = Dumpglob.dump_definition lid false "def"; (match expr with | ProveBody (bl, t) -> - start_proof_and_print env isevars (Some lid) - (pi1 defkind, pi2 defkind, DefinitionBody Definition) (bl,t) + start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) @@ -149,7 +148,7 @@ let subtac (loc, command) = let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l) - | VernacStartTheoremProof (thkind, p, [Some id, (bl,t,guard)], lettop, hook) -> + | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> if guard <> None then error "Do not support building theorems as a fixpoint."; Dumpglob.dump_definition id false "prf"; @@ -161,12 +160,12 @@ let subtac (loc, command) = errorlabstrm "Subtac_command.StartProof" (str "Proof editing mode not supported in module types"); check_fresh id; - start_proof_and_print env isevars (Some id) (Global, p, Proof thkind) (bl,t) hook + start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook | VernacAssumption (stre,nl,l) -> vernac_assumption env isevars stre l nl - | VernacInstance (abst, glob, poly, sup, is, props, pri) -> + | VernacInstance (abst, glob, sup, is, props, pri) -> dump_constraint "inst" is; if abst then error "Declare Instance not supported here."; diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 0a3da4d0c..05e634c58 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -180,4 +180,4 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p in let evm = Subtac_utils.evars_of_term !evars Evd.empty term in let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in - id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls + id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 5c7f7b5ec..f02e83ad1 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -327,7 +327,6 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let ce = { const_entry_body = Evarutil.nf_evar !isevars body; const_entry_type = Some ty; - const_entry_polymorphic = false; const_entry_opaque = false } in let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 874cce85c..76cc7644d 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -231,11 +231,10 @@ let subst_body expand prg = let declare_definition prg = let body, typ = subst_body true prg in - let (local, poly, kind) = prg.prg_kind in + let (local, kind) = prg.prg_kind in let ce = { const_entry_body = body; const_entry_type = Some typ; - const_entry_polymorphic = poly; const_entry_opaque = false } in (Command.get_declare_definition_hook ()) ce; @@ -254,7 +253,7 @@ let declare_definition prg = | (Global|Local) -> let c = Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind)) + prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind)) in let gr = ConstRef c in if Impargs.is_implicit_args () || prg.prg_implicits <> [] then @@ -302,7 +301,7 @@ let declare_mutual_definition l = let fixkind = Option.get first.prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in - let (local,poly,kind) = first.prg_kind in + let (local,kind) = first.prg_kind in let fixnames = first.prg_deps in let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in let indexes, fixdecls = @@ -335,7 +334,6 @@ let declare_obligation prg obl body = let ce = { const_entry_body = body; const_entry_type = Some ty; - const_entry_polymorphic = false; const_entry_opaque = opaque } in let constant = Declare.declare_constant obl.obl_name @@ -604,7 +602,7 @@ let show_term n = my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ my_print_constr (Global.env ()) prg.prg_body) -let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic +let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls = Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in @@ -622,7 +620,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) +let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce) ?(hook=fun _ _ -> ()) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in let upd = List.fold_left diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 6487a14b7..7fba23dc2 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -218,13 +218,13 @@ let non_instanciated_map env evd evm = Evd.empty (Evarutil.non_instantiated evm) let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition -let goal_kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Definition +let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma -let goal_proof_kind = Decl_kinds.Global, false, Decl_kinds.Proof Decl_kinds.Lemma +let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint -let goal_fix_kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint +let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint open Tactics open Tacticals diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index d2c3fd0c8..2753a2522 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -95,11 +95,11 @@ val string_of_hole_kind : hole_kind -> string val evars_of_term : evar_map -> evar_map -> constr -> evar_map val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map val global_kind : logical_kind -val goal_kind : locality * polymorphic * goal_object_kind +val goal_kind : locality * goal_object_kind val global_proof_kind : logical_kind -val goal_proof_kind : locality * polymorphic * goal_object_kind +val goal_proof_kind : locality * goal_object_kind val global_fix_kind : logical_kind -val goal_fix_kind : locality * polymorphic * goal_object_kind +val goal_fix_kind : locality * goal_object_kind val mkSubset : name -> constr -> constr -> constr val mkProj1 : constr -> constr -> constr -> constr diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e953d2074..fff1a121d 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -151,7 +151,7 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id sign typ tac = - start_proof id (Global,false,Proof Theorem) sign typ (fun _ _ -> ()); + start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ()); try by tac; let _,(const,_,_,_) = cook_proof (fun _ -> ()) in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fa108f1ec..bcd9d6e0d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -265,18 +265,16 @@ let close_proof () = let id = get_current_proof_name () in let p = give_me_the_proof () in let proofs_and_types = Proof.return p in - let { compute_guard=cg ; strength=str ; hook=hook } = - Idmap.find id !proof_info - in - let (_, poly, _) = str in let entries = List.map (fun (c,t) -> { Entries.const_entry_body = c ; const_entry_type = Some t; - const_entry_polymorphic = poly; const_entry_opaque = true }) proofs_and_types in - (id,(entries,cg,str,hook)) + let { compute_guard=cg ; strength=str ; hook=hook } = + Idmap.find id !proof_info + in + (id, (entries,cg,str,hook)) with | Proof.UnfinishedProof -> Util.error "Attempt to save an incomplete proof" diff --git a/tactics/leminv.ml b/tactics/leminv.ml index b06810a8c..95814302d 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -236,7 +236,6 @@ let add_inversion_lemma name env sigma t sort dep inv_op = (DefinitionEntry { const_entry_body = invProof; const_entry_type = None; - const_entry_polymorphic = true; const_entry_opaque = false }, IsProof Lemma) in () diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index a01799b18..c633a9c0d 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1438,7 +1438,7 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance false binders instance (Some (CRecord (dummy_loc,None,fields))) + new_instance binders instance (Some (CRecord (dummy_loc,None,fields))) ~global:(not (Vernacexpr.use_section_locality ())) ~generalize:false None let declare_instance_refl global binders a aeq n lemma = @@ -1617,7 +1617,6 @@ let declare_projection n instance_id r = let cst = { const_entry_body = term; const_entry_type = Some typ; - const_entry_polymorphic = false; const_entry_opaque = false } in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) @@ -1688,7 +1687,7 @@ let add_morphism_infer glob m n = add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) else - let kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Instance in + let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> Lemmas.start_proof instance_id kind instance @@ -1711,7 +1710,7 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in - ignore(new_instance ~global:glob false binders instance (Some (CRecord (dummy_loc,None,[]))) + ignore(new_instance ~global:glob binders instance (Some (CRecord (dummy_loc,None,[]))) ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) VERNAC COMMAND EXTEND AddSetoid1 diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b33942b0c..46428236c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1238,7 +1238,7 @@ let solvable_by_tactic env evi (ev,args) src = Environ.named_context_of_val evi.evar_hyps = Environ.named_context env -> let id = id_of_string "H" in - start_proof id (Local,false,Proof Lemma) evi.evar_hyps evi.evar_concl + start_proof id (Local,Proof Lemma) evi.evar_hyps evi.evar_concl (fun _ _ -> ()); begin try diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 1ce74f472..56cab0f68 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -9,95 +9,4 @@ End S. (* Check f nat nat : Set. *) -Check I nat nat : Set. - -Definition I' (B : Type) := I B. - -Check I' nat nat : Set. - -Definition I'' (B : Type) := (I B B * I B B)%type. -Set Printing Universes. -Check I'' nat. -Definition id {A : Type} (a : A) := a. -Definition crelation (A:Type) := A -> A -> Type. -Print crelation. -Polymorphic Definition pcrelation (A:Type) := A -> A -> Type. -Print pcrelation. -Definition TYPE := Type. -Print TYPE. -Check crelation TYPE. -Check pcrelation TYPE. -Check pcrelation (pcrelation TYPE). - -Definition foo := crelation TYPE. -Check crelation foo. - -Class Category (obj : Type) (hom : crelation obj) := { - id_obj o : hom o o ; - comp {o o' o''} : hom o' o'' -> hom o o' -> hom o o'' ; - comp_id_l o o' (f : hom o' o) : comp (id_obj o) f = f ; - comp_id_r o o' (f : hom o o') : comp f (id_obj o) = f }. -Class Functor {A H B H'} (C : Category A H) (D : Category B H') := { - fmap : A -> B; - fmap_F {a b} : H a b -> H' (fmap a) (fmap b) ; - fmap_id a : fmap_F (id_obj a) = id_obj (fmap a) - -}. - - -Instance TYPE_cat : Category TYPE (fun a b => a -> b) := - { id_obj o := id; comp o o' o'' g f := fun x => g (f x) }. - -Instance ID_Functor {A H} (C : Category A H) : Functor C C := { - fmap a := a ; - fmap_F a b f := f }. -Proof. reflexivity. Qed. - -Record category := { - obj : Type ; hom : crelation obj; cat : Category obj hom }. - -Record functor (c d : category) := mkFunctor { - funct : Functor (cat c) (cat d) }. - -Instance functor_cat : Category category functor. admit. Qed. - -(* := { *) -(* id_obj o := mkFunctor _ _ (ID_Functor (cat o)); *) -(* comp o o' o'' := _ *) -(* }. *) -(* Proof. admit. intros. constructor. apply (ID_Functor (cat o)). admit. *) - -(* Qed. *) - -Class nat_trans {A H B H'} (C : Category A H) (D : Category B H') (F G : Functor C D) := { - nat_transform o : H' (fmap (Functor:=F) o) (fmap (Functor:=G) o) ; - nat_natural X Y (f : H X Y) : comp (nat_transform Y) (fmap_F (Functor:=F) f) = - comp (fmap_F (Functor:=G) f) (nat_transform X) -}. - -Record nat_transf {C D} (F G : functor C D) := mkNatTransf { - nat_transfo : nat_trans (cat C) (cat D) (funct _ _ F) (funct _ _ G) }. - -Instance id_nat_trans {A H B H'} (C : Category A H) (D : Category B H') (F : Functor C D) : - nat_trans _ _ F F := - { nat_transform o := fmap_F (id_obj o) }. -Proof. intros. rewrite !fmap_id, comp_id_l, comp_id_r. reflexivity. Qed. - -Instance nat_trans_cat C D : Category (functor C D) (@nat_transf C D) := - { id_obj o := {| nat_transfo := id_nat_trans _ _ (funct _ _ o) |} }. -Proof. simpl. - - -Polymorphic De -Print TYPE. -Check (id (A:=TYPE)). -Check (id (A:=Type)). -Check (id (id (A:=TYPE))). - -Definition TYPE1 := TYPE. -Print TYPE. Print TYPE1. -Check I'' TYPE. -Check I'' TYPE. - - -Print I''. Print I. +Check I nat nat : Set.
\ No newline at end of file diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 7027b89ee..af1330a42 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -181,7 +181,6 @@ let declare_record_instance gr ctx params = let def = deep_refresh_universes def in let ce = { const_entry_body=def; const_entry_type=None; - const_entry_polymorphic = true; const_entry_opaque=false } in let cst = Declare.declare_constant ident (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in @@ -197,7 +196,6 @@ let declare_class_instance gr ctx params = let ce = Entries.DefinitionEntry { const_entry_type=Some typ; const_entry_body=def; - const_entry_polymorphic=true; const_entry_opaque=false } in try let cst = Declare.declare_constant ident diff --git a/toplevel/class.ml b/toplevel/class.ml index 77b49b4bd..4e729f446 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -218,7 +218,6 @@ let build_id_coercion idf_opt source = DefinitionEntry { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); const_entry_type = Some typ_f; - const_entry_polymorphic = false; const_entry_opaque = false } in let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in ConstRef kn diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 9535e9aaa..8d7581179 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -104,13 +104,12 @@ let instance_hook k pri global imps ?hook cst = Typeclasses.add_instance inst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant k pri global imps ?hook poly id term termtype = +let declare_instance_constant k pri global imps ?hook id term termtype = let cdecl = let kind = IsDefinition Instance in let entry = { const_entry_body = term; const_entry_type = Some termtype; - const_entry_polymorphic = poly; const_entry_opaque = false } in DefinitionEntry entry, kind in @@ -119,7 +118,7 @@ let declare_instance_constant k pri global imps ?hook poly id term termtype = instance_hook k pri global imps ?hook (ConstRef kn); id -let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props +let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) ?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri = let env = Global.env() in @@ -255,10 +254,10 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro let evm = undefined_evars !evars in Evarutil.check_evars env Evd.empty !evars termtype; if Evd.is_empty evm && term <> None then - declare_instance_constant k pri global imps ?hook poly id (Option.get term) termtype + declare_instance_constant k pri global imps ?hook id (Option.get term) termtype else begin evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars; - let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in + let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook); if term <> None then @@ -300,7 +299,6 @@ let rec declare_subclasses gr (rels, (tc, args)) = let ce = { const_entry_body = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels; const_entry_type = None; - const_entry_polymorphic = false; const_entry_opaque = false } in let cst = Declare.declare_constant ~internal:Declare.KernelSilent @@ -341,7 +339,7 @@ let context l = (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls in - Command.declare_assumption false (Local (* global *), false, Definitional) t + Command.declare_assumption false (Local (* global *), Definitional) t [] impl (* implicit *) None (* inline *) (dummy_loc, id)) (* match class_of_constr t with *) (* | None -> () *) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 5ef5feffd..b57f1bea0 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -40,7 +40,6 @@ val declare_instance_constant : bool -> (** globality *) Impargs.manual_explicitation list -> (** implicits *) ?hook:(Libnames.global_reference -> unit) -> - polymorphic -> identifier -> (** name *) Term.constr -> (** body *) Term.types -> (** type *) @@ -49,7 +48,6 @@ val declare_instance_constant : val new_instance : ?abstract:bool -> (** Not abstract by default. *) ?global:bool -> (** Not global by default. *) - polymorphic -> local_binder list -> typeclass_constraint -> constr_expr option -> diff --git a/toplevel/command.ml b/toplevel/command.ml index ea606210b..90376a431 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -64,7 +64,7 @@ let red_constant_entry n ce = function { ce with const_entry_body = under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body } -let interp_definition bl p red_option c ctypopt = +let interp_definition bl red_option c ctypopt = let env = Global.env() in let evdref = ref Evd.empty in let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in @@ -78,7 +78,6 @@ let interp_definition bl p red_option c ctypopt = imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; const_entry_type = None; - const_entry_polymorphic = p; const_entry_opaque = false } | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in @@ -90,7 +89,6 @@ let interp_definition bl p red_option c ctypopt = imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; const_entry_type = Some typ; - const_entry_polymorphic = p; const_entry_opaque = false } in red_constant_entry (rel_context_length ctx) ce red_option, imps @@ -128,7 +126,7 @@ let declare_definition ident (local,k) ce imps hook = (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let declare_assumption is_coe (local,p,kind) c imps impl nl (_,ident) = +let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = @@ -474,7 +472,6 @@ let declare_fix kind f def t imps = let ce = { const_entry_body = def; const_entry_type = Some t; - const_entry_polymorphic = false; const_entry_opaque = false } in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in @@ -554,7 +551,7 @@ let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in - Lemmas.start_proof_with_initialization (Global,false,DefinitionBody Fixpoint) + Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint) (Some(false,indexes,init_tac)) thms None (fun _ _ -> ()) else begin (* We shortcut the proof process *) @@ -579,7 +576,7 @@ let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns = let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in - Lemmas.start_proof_with_initialization (Global,false,DefinitionBody CoFixpoint) + Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint) (Some(true,[],init_tac)) thms None (fun _ _ -> ()) else begin (* We shortcut the proof process *) diff --git a/toplevel/command.mli b/toplevel/command.mli index 0430e401a..8ffdbdec4 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -31,7 +31,7 @@ val set_declare_assumptions_hook : (types -> unit) -> unit (** {6 Definitions/Let} *) val interp_definition : - local_binder list -> polymorphic -> red_expr option -> constr_expr -> + local_binder list -> red_expr option -> constr_expr -> constr_expr option -> definition_entry * Impargs.manual_implicits val declare_definition : identifier -> locality * definition_object_kind -> diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 33a842449..51dc1dc30 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -115,7 +115,6 @@ let define internal id c = (DefinitionEntry { const_entry_body = c; const_entry_type = None; - const_entry_polymorphic = true; const_entry_opaque = false }, Decl_kinds.IsDefinition Scheme) in (match internal with diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index b280836af..52c9be675 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -105,7 +105,6 @@ let define id internal c t = (DefinitionEntry { const_entry_body = c; const_entry_type = t; - const_entry_polymorphic = true; const_entry_opaque = false }, Decl_kinds.IsDefinition Scheme) in definition_message id; diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index a72a6b5ab..7f3edefbb 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -155,7 +155,7 @@ let look_for_possibly_mutual_statements = function (* Saving a goal *) -let save id const do_guard (locality,poly,kind) hook = +let save id const do_guard (locality,kind) hook = let const = adjust_guardness_conditions const do_guard in let {const_entry_body = pft; const_entry_type = tpo; @@ -187,7 +187,7 @@ let compute_proof_name locality = function | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) -let save_remaining_recthms (local,p,kind) body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) = match body with | None -> (match local with @@ -216,7 +216,6 @@ let save_remaining_recthms (local,p,kind) body opaq i (id,(t_i,(_,imps))) = let const = { const_entry_body = body_i; const_entry_type = Some t_i; - const_entry_polymorphic = p; const_entry_opaque = opaq } in let kn = declare_constant id (DefinitionEntry const, k) in (Global,ConstRef kn,imps) @@ -245,7 +244,7 @@ let save_anonymous_with_strength kind opacity save_ident = let id,const,do_guard,_,hook = get_proof opacity in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) - save save_ident const do_guard (Global, const.const_entry_polymorphic, Proof kind) hook + save save_ident const do_guard (Global, Proof kind) hook (* Starting a goal *) @@ -318,7 +317,7 @@ let start_proof_com kind thms hook = let t', imps' = interp_type_evars_impls ~impls ~evdref env t in Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx; let ids = List.map pi1 ctx in - (compute_proof_name (pi1 kind) sopt, + (compute_proof_name (fst kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), guard))) diff --git a/toplevel/record.ml b/toplevel/record.ml index bcaf86ae3..36d29c1a1 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -201,7 +201,6 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let cie = { const_entry_body = proj; const_entry_type = Some projtyp; - const_entry_polymorphic = true; const_entry_opaque = false } in let k = (DefinitionEntry cie,IsDefinition kind) in let kn = declare_constant ~internal:KernelSilent fid k in @@ -311,7 +310,6 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let class_entry = { const_entry_body = class_body; const_entry_type = class_type; - const_entry_polymorphic = true; const_entry_opaque = false } in let cst = Declare.declare_constant (snd id) @@ -323,7 +321,6 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let proj_entry = { const_entry_body = proj_body; const_entry_type = Some proj_type; - const_entry_polymorphic = true; const_entry_opaque = false } in let proj_cst = Declare.declare_constant proj_name diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2ed871d1e..088fb3b96 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -329,13 +329,13 @@ let start_proof_and_print k l hook = print_subgoals (); if !pcoq <> None then (Option.get !pcoq).start_proof () -let vernac_definition (local,p,k) (loc,id as lid) def hook = +let vernac_definition (local,k) (loc,id as lid) def hook = if local = Local then Dumpglob.dump_definition lid true "var" else Dumpglob.dump_definition lid false "def"; (match def with | ProveBody (bl,t) -> (* local binders, typ *) let hook _ _ = () in - start_proof_and_print (local,p,DefinitionBody Definition) + start_proof_and_print (local,DefinitionBody Definition) [Some lid, (bl,t,None)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with @@ -343,10 +343,10 @@ let vernac_definition (local,p,k) (loc,id as lid) def hook = | Some r -> let (evc,env)= get_current_context () in Some (interp_redexp env evc r) in - let ce,imps = interp_definition bl p red_option c typ_opt in + let ce,imps = interp_definition bl red_option c typ_opt in declare_definition id (local,k) ce imps hook) -let vernac_start_proof kind p l lettop hook = +let vernac_start_proof kind l lettop hook = if Dumpglob.dump () then List.iter (fun (id, _) -> match id with @@ -356,7 +356,7 @@ let vernac_start_proof kind p l lettop hook = if lettop then errorlabstrm "Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode."); - start_proof_and_print (Global, p, Proof kind) l hook + start_proof_and_print (Global, Proof kind) l hook let vernac_end_proof = function | Admitted -> admit () @@ -380,7 +380,7 @@ let vernac_assumption kind l nl= if Pfedit.refining () then errorlabstrm "" (str "Cannot declare an assumption while in proof editing mode."); - let global = Util.pi1 kind = Global in + let global = fst kind = Global in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun lid -> @@ -628,9 +628,9 @@ let vernac_identity_coercion stre id qids qidt = (* Type classes *) -let vernac_instance abst glob poly sup inst props pri = +let vernac_instance abst glob sup inst props pri = Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~abstract:abst ~global:glob poly sup inst props pri) + ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri) let vernac_context l = Classes.context l @@ -1334,7 +1334,7 @@ let interp c = match c with (* Gallina *) | VernacDefinition (k,lid,d,f) -> vernac_definition k lid d f - | VernacStartTheoremProof (k,p,l,top,f) -> vernac_start_proof k p l top f + | VernacStartTheoremProof (k,l,top,f) -> vernac_start_proof k l top f | VernacEndProof e -> vernac_end_proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl @@ -1365,8 +1365,8 @@ let interp c = match c with | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t (* Type classes *) - | VernacInstance (abst, glob, poly, sup, inst, props, pri) -> - vernac_instance abst glob poly sup inst props pri + | VernacInstance (abst, glob, sup, inst, props, pri) -> + vernac_instance abst glob sup inst props pri | VernacContext sup -> vernac_context sup | VernacDeclareInstances (glob, ids) -> vernac_declare_instances glob ids | VernacDeclareClass id -> vernac_declare_class id @@ -1420,7 +1420,7 @@ let interp c = match c with | VernacNop -> () (* Proof management *) - | VernacGoal t -> vernac_start_proof Theorem false [None,([],t,None)] false (fun _ _->()) + | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] false (fun _ _->()) | VernacAbort id -> vernac_abort id | VernacAbortAll -> vernac_abort_all () | VernacRestart -> vernac_restart () diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 9bd6bb1b0..216306f5e 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -223,9 +223,9 @@ type vernac_expr = scope_name option (* Gallina *) - | VernacDefinition of definition_kind - * lident * definition_expr * declaration_hook - | VernacStartTheoremProof of theorem_kind * polymorphic * + | VernacDefinition of definition_kind * lident * definition_expr * + declaration_hook + | VernacStartTheoremProof of theorem_kind * (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list * bool * declaration_hook | VernacEndProof of proof_end @@ -253,7 +253,6 @@ type vernac_expr = | VernacInstance of bool * (* abstract instance *) bool * (* global *) - bool * (* polymorphic *) local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) constr_expr option * (* props *) |