diff options
42 files changed, 262 insertions, 132 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 02330339d..8c52655ff 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_if_constant_for_ind env j + Typeops.make_polymorphic env j in (body, typ, cb.const_constraints) diff --git a/kernel/entries.ml b/kernel/entries.ml index 28f11c9af..32dfaae8f 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -55,9 +55,10 @@ type mutual_inductive_entry = { (*s Constants (Definition/Axiom) *) type definition_entry = { - const_entry_body : constr; - const_entry_type : types option; - const_entry_opaque : bool } + const_entry_body : constr; + const_entry_type : types option; + const_entry_polymorphic : bool; + 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 08740afae..5d9569de4 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -51,9 +51,10 @@ type mutual_inductive_entry = { (** {6 Constants (Definition/Axiom) } *) type definition_entry = { - const_entry_body : constr; - const_entry_type : types option; - const_entry_opaque : bool } + const_entry_body : constr; + const_entry_type : types option; + const_entry_polymorphic : bool; + 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 8146ea7c1..9a73abfad 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -26,14 +26,17 @@ open Type_errors open Indtypes open Typeops -let constrain_type env j cst1 = function - | None -> - make_polymorphic_if_constant_for_ind env j, cst1 +let constrain_type env j cst1 poly = function + | None -> make_polymorphic env j, cst1 | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in - assert (t = tj.utj_val); - NonPolymorphicType t, union_constraints (union_constraints cst1 cst2) cst3 + assert (t = tj.utj_val); + let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in + if poly then + make_polymorphic env { j with uj_type = tj.utj_val }, cstrs + else + NonPolymorphicType t, cstrs let local_constrain_type env j cst1 = function | None -> @@ -92,7 +95,8 @@ 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_type in + let (typ,cst) = constrain_type env j cst + c.const_entry_polymorphic c.const_entry_type 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 85e8e6c88..b7a8b7d4e 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_if_constant_for_ind env {uj_val = c; uj_type = t} = +let make_polymorphic 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) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> + | Sort (Type u) -> 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 c1c805f38..af46b9875 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -101,6 +101,5 @@ val type_of_constant_knowing_parameters : env -> constant_type -> constr array -> types (** Make a type polymorphic if an arity *) -val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> - constant_type +val make_polymorphic : env -> unsafe_judgment -> constant_type diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index ba40f98c0..bdc855869 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -15,6 +15,8 @@ type locality = | Local | Global +type polymorphic = bool + type theorem_kind = | Theorem | Lemma @@ -48,9 +50,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * assumption_object_kind +type assumption_kind = locality * polymorphic * assumption_object_kind -type definition_kind = locality * definition_object_kind +type definition_kind = locality * polymorphic * definition_object_kind (* Kinds used in proofs *) @@ -58,7 +60,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * goal_object_kind +type goal_kind = locality * polymorphic * goal_object_kind (* Kinds used in library *) @@ -82,22 +84,23 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -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" +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 (* Strength *) diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 88ef763c9..1e4ad07e8 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -15,6 +15,8 @@ type locality = | Local | Global +type polymorphic = bool + type theorem_kind = | Theorem | Lemma @@ -48,9 +50,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * assumption_object_kind +type assumption_kind = locality * polymorphic * assumption_object_kind -type definition_kind = locality * definition_object_kind +type definition_kind = locality * polymorphic * definition_object_kind (** Kinds used in proofs *) @@ -58,7 +60,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * goal_object_kind +type goal_kind = locality * polymorphic * goal_object_kind (** Kinds used in library *) @@ -72,7 +74,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 * definition_object_kind -> string + locality * polymorphic * definition_object_kind -> string (** About locality *) diff --git a/library/declare.ml b/library/declare.ml index c566cedfd..ec713d5b2 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -160,7 +160,8 @@ 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_opaque = ce.const_entry_opaque } + const_entry_polymorphic = ce.const_entry_polymorphic; + 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 160d94130..73c3ca8c0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -135,25 +135,36 @@ 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,(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 -> + 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 -> test_plurial_form bl; - VernacAssumption (stre, nl, bl) - | (f,d) = def_token; id = identref; b = def_body -> - VernacDefinition (d, id, b, f) + 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) (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> @@ -520,16 +531,16 @@ GEXTEND Gram d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition - ((Global,CanonicalStructure),(dummy_loc,s),d, + ((Global,false,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 (),Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((use_locality_exp (),false,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,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((enforce_locality_exp true,false,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) @@ -557,7 +568,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 ()), + VernacInstance (false, not (use_section_locality ()), false, snd namesup, (fst namesup, expl, t), props, pri) | IDENT "Existing"; IDENT "Instance"; id = global -> @@ -628,7 +639,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 ()), + VernacInstance (true, not (use_section_locality ()), false, snd namesup, (fst namesup, expl, t), None, pri) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 4bf6e59f1..d21b83ab6 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -347,18 +347,20 @@ let pr_class_rawexpr = function | SortClass -> str"Sortclass" | RefClass qid -> pr_smart_global qid -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_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_params pr_c (xl,(c,t)) = hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ @@ -569,7 +571,7 @@ let rec pr_vernac = function | None -> mt() | Some cc -> str" :=" ++ spc() ++ cc)) - | VernacStartTheoremProof (ki,l,_,_) -> + | VernacStartTheoremProof (ki,p,l,_,_) -> hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ prlist (pr_statement (spc () ++ str "with")) (List.tl l)) @@ -690,10 +692,11 @@ 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, sup, (instid, bk, cl), props, pri) -> + | VernacInstance (abst,glob,poly,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 4f32bbd99..c1b3c0b84 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,(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global, false, (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 2ba29ced7..d3949731b 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,(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) new_principle_type (hook new_principle_type) ; @@ -382,6 +382,7 @@ 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 dd48765fb..0e4dd1289 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 None body (Some ret_type) + Command.interp_definition bl false 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 094d2e50f..a0d2061bc 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,kind) hook = +let save with_clean id const (locality,p,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 426b496dd..ce484ca23 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,(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,false,(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,(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global, false, (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 11fbc01ba..24379e7b4 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, Decl_kinds.Proof Decl_kinds.Lemma) + (Decl_kinds.Global, false, 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, Proof Lemma) (Environ.named_context_val env) + (Global, false, Proof Lemma) (Environ.named_context_val env) (hyp_terminates nb_args fonctional_ref) hook; by (observe_tac "starting_tac" tac_start); @@ -1140,6 +1140,7 @@ 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));; @@ -1349,7 +1350,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, Proof Lemma) + (start_proof eq_name (Global, false, 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 38c65cdd0..d434a890f 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -159,6 +159,7 @@ 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 fbdaa8d3b..7faf78033 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 = fst kind = Global in + let global = pi1 kind = Global in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun lid -> @@ -137,7 +137,8 @@ let subtac (loc, command) = Dumpglob.dump_definition lid false "def"; (match expr with | ProveBody (bl, t) -> - start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) + start_proof_and_print env isevars (Some lid) + (pi1 defkind, pi2 defkind, DefinitionBody Definition) (bl,t) (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) @@ -148,7 +149,7 @@ let subtac (loc, command) = let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l) - | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> + | VernacStartTheoremProof (thkind, p, [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"; @@ -160,12 +161,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, Proof thkind) (bl,t) hook + start_proof_and_print env isevars (Some id) (Global, p, Proof thkind) (bl,t) hook | VernacAssumption (stre,nl,l) -> vernac_assumption env isevars stre l nl - | VernacInstance (abst, glob, sup, is, props, pri) -> + | VernacInstance (abst, glob, poly, 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 05e634c58..0a3da4d0c 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,Instance) ~hook obls + id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index f02e83ad1..5c7f7b5ec 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -327,6 +327,7 @@ 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 76cc7644d..874cce85c 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -231,10 +231,11 @@ let subst_body expand prg = let declare_definition prg = let body, typ = subst_body true prg in - let (local, kind) = prg.prg_kind in + let (local, poly, 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; @@ -253,7 +254,7 @@ let declare_definition prg = | (Global|Local) -> let c = Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind)) + prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind)) in let gr = ConstRef c in if Impargs.is_implicit_args () || prg.prg_implicits <> [] then @@ -301,7 +302,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,kind) = first.prg_kind in + let (local,poly,kind) = first.prg_kind in let fixnames = first.prg_deps in let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in let indexes, fixdecls = @@ -334,6 +335,7 @@ 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 @@ -602,7 +604,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,Definition) ?tactic +let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,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 @@ -620,7 +622,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce) +let add_mutual_definitions l ?tactic ?(kind=Global,false,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 7fba23dc2..6487a14b7 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, Decl_kinds.DefinitionBody Decl_kinds.Definition +let goal_kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Definition let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma -let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma +let goal_proof_kind = Decl_kinds.Global, false, Decl_kinds.Proof Decl_kinds.Lemma let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint -let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint +let goal_fix_kind = Decl_kinds.Global, false, 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 2753a2522..d2c3fd0c8 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 * goal_object_kind +val goal_kind : locality * polymorphic * goal_object_kind val global_proof_kind : logical_kind -val goal_proof_kind : locality * goal_object_kind +val goal_proof_kind : locality * polymorphic * goal_object_kind val global_fix_kind : logical_kind -val goal_fix_kind : locality * goal_object_kind +val goal_fix_kind : locality * polymorphic * 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 fff1a121d..e953d2074 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,Proof Theorem) sign typ (fun _ _ -> ()); + start_proof id (Global,false,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 bcd9d6e0d..fa108f1ec 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -265,16 +265,18 @@ 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 - let { compute_guard=cg ; strength=str ; hook=hook } = - Idmap.find id !proof_info - in - (id, (entries,cg,str,hook)) + (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 95814302d..b06810a8c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -236,6 +236,7 @@ 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 9ad419697..4d8fc0e44 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 binders instance (Some (CRecord (dummy_loc,None,fields))) + new_instance false 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,6 +1617,7 @@ 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)) @@ -1687,7 +1688,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, Decl_kinds.DefinitionBody Decl_kinds.Instance in + let kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> Lemmas.start_proof instance_id kind instance @@ -1710,7 +1711,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 binders instance (Some (CRecord (dummy_loc,None,[]))) + ignore(new_instance ~global:glob false 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 505ab161b..735de9371 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,Proof Lemma) evi.evar_hyps evi.evar_concl + start_proof id (Local,false,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 5a008f18b..a9b9cc18e 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -10,3 +10,80 @@ 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'' +}. +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) +}. + + +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 }. + + +Record category := { + obj : Type ; hom : crelation obj; cat : Category obj hom }. + +Record functor (c d : category) := { + funct : Functor (cat c) (cat d) }. + +Instance functor_cat : Category category functor. +Proof. constructor. 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) := { + nat_transfo : nat_trans (cat C) (cat D) (funct _ _ F) (funct _ _ G) }. + +Instance nat_trans_cat C D : Category (functor C D) (@nat_transf C D). +Proof. admit. Qed. + + +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. diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index af1330a42..7027b89ee 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -181,6 +181,7 @@ 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 @@ -196,6 +197,7 @@ 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 4e729f446..77b49b4bd 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -218,6 +218,7 @@ 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 7786b200b..200bc516a 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -102,12 +102,13 @@ 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 id term termtype = +let declare_instance_constant k pri global imps ?hook poly 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 @@ -116,7 +117,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype = instance_hook k pri global imps ?hook (ConstRef kn); id -let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props +let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri = let env = Global.env() in @@ -252,10 +253,10 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props 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 id (Option.get term) termtype + declare_instance_constant k pri global imps ?hook poly id (Option.get term) termtype else begin evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars; - let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in + let kind = Decl_kinds.Global, poly, 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 @@ -297,6 +298,7 @@ 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 @@ -337,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 *), Definitional) t + Command.declare_assumption false (Local (* global *), false, 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 b57f1bea0..5ef5feffd 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -40,6 +40,7 @@ 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 *) @@ -48,6 +49,7 @@ 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 90376a431..ea606210b 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 red_option c ctypopt = +let interp_definition bl p 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,6 +78,7 @@ let interp_definition bl 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 @@ -89,6 +90,7 @@ let interp_definition bl 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 @@ -126,7 +128,7 @@ let declare_definition ident (local,k) ce imps hook = (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = +let declare_assumption is_coe (local,p,kind) c imps impl nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = @@ -472,6 +474,7 @@ 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 @@ -551,7 +554,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,DefinitionBody Fixpoint) + Lemmas.start_proof_with_initialization (Global,false,DefinitionBody Fixpoint) (Some(false,indexes,init_tac)) thms None (fun _ _ -> ()) else begin (* We shortcut the proof process *) @@ -576,7 +579,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,DefinitionBody CoFixpoint) + Lemmas.start_proof_with_initialization (Global,false,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 8ffdbdec4..0430e401a 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 -> red_expr option -> constr_expr -> + local_binder list -> polymorphic -> 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 51dc1dc30..33a842449 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -115,6 +115,7 @@ 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 52c9be675..b280836af 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -105,6 +105,7 @@ 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 7cc9ba33e..7e806cf10 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,kind) hook = +let save id const do_guard (locality,poly,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,kind) body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (local,p,kind) body opaq i (id,(t_i,(_,imps))) = match body with | None -> (match local with @@ -216,6 +216,7 @@ let save_remaining_recthms (local,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) @@ -244,7 +245,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, Proof kind) hook + save save_ident const do_guard (Global, const.const_entry_polymorphic, Proof kind) hook (* Starting a goal *) @@ -317,7 +318,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 (fst kind) sopt, + (compute_proof_name (pi1 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 36d29c1a1..bcaf86ae3 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -201,6 +201,7 @@ 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 @@ -310,6 +311,7 @@ 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) @@ -321,6 +323,7 @@ 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 088fb3b96..2ed871d1e 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,k) (loc,id as lid) def hook = +let vernac_definition (local,p,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,DefinitionBody Definition) + start_proof_and_print (local,p,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,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 red_option c typ_opt in + let ce,imps = interp_definition bl p red_option c typ_opt in declare_definition id (local,k) ce imps hook) -let vernac_start_proof kind l lettop hook = +let vernac_start_proof kind p l lettop hook = if Dumpglob.dump () then List.iter (fun (id, _) -> match id with @@ -356,7 +356,7 @@ let vernac_start_proof kind 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, Proof kind) l hook + start_proof_and_print (Global, p, 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 = fst kind = Global in + let global = Util.pi1 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 sup inst props pri = +let vernac_instance abst glob poly sup inst props pri = Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri) + ignore(Classes.new_instance ~abstract:abst ~global:glob poly 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,l,top,f) -> vernac_start_proof k l top f + | VernacStartTheoremProof (k,p,l,top,f) -> vernac_start_proof k p 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, sup, inst, props, pri) -> - vernac_instance abst glob sup inst props pri + | VernacInstance (abst, glob, poly, sup, inst, props, pri) -> + vernac_instance abst glob poly 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 [None,([],t,None)] false (fun _ _->()) + | VernacGoal t -> vernac_start_proof Theorem false [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 216306f5e..9bd6bb1b0 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 * + | VernacDefinition of definition_kind + * lident * definition_expr * declaration_hook + | VernacStartTheoremProof of theorem_kind * polymorphic * (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list * bool * declaration_hook | VernacEndProof of proof_end @@ -253,6 +253,7 @@ 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 *) |