diff options
| author | Enrico Tassi | 2019-05-24 14:57:33 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:43 +0200 |
| commit | a7a6fa3219134004f1fc6c757f1c16281724f38f (patch) | |
| tree | 3d0653067a9ea3c574b6237f6f8d0c5adae72450 /plugins/ltac | |
| parent | d77604cb06fcc8e8f38ef979627aa7a7138ef0f2 (diff) | |
[vernac] more precise types for Add Morph, Instance, and Function
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c568f63903..caeedadbf4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1796,11 +1796,11 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance atts binders (name,t) fields = let program_mode = atts.program in - let _id, proof = Classes.new_instance ~program_mode atts.polymorphic - name binders t (Some (true, CAst.make @@ CRecord (fields))) + let _id = Classes.new_instance ~program_mode atts.polymorphic + name binders t (true, CAst.make @@ CRecord (fields)) ~global:atts.global ~generalize:false Hints.empty_hint_info in - assert (Option.is_empty proof) (* refine:false with term *) + () let declare_instance_refl atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" @@ -2024,12 +2024,12 @@ let add_morphism atts binders m s n = [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = Classes.new_instance + let _id, pstate = Classes.new_instance_interactive ~program_mode:atts.program ~global:atts.global atts.polymorphic - instance_name binders instance_t None + instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - Option.get pstate (* no instance body -> always open proof *) + pstate (* no instance body -> always open proof *) (** Bind to "rewrite" too *) |