diff options
| author | msozeau | 2011-04-13 14:29:02 +0000 |
|---|---|---|
| committer | msozeau | 2011-04-13 14:29:02 +0000 |
| commit | 60bc3cbe72083f4fa1aa759914936e4fa3d6b42e (patch) | |
| tree | 0eeffe9b7b098ad653ffeb6ad963c62223245d0e /toplevel/classes.ml | |
| parent | 3b11686e4f78f6d166f84d990ac4fedb4d3e800a (diff) | |
Revert "Add [Polymorphic] flag for defs"
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719.
Conflicts:
kernel/term_typing.ml
test-suite/success/polymorphism.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 9535e9aaaf..8d7581179b 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 -> () *) |