diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index b5adc66640..52c4837716 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -93,8 +93,8 @@ let empty_se = ([],[],Btermdn.create ()) let add_tac t (l,l',dn) = match t.pat with - None -> (insert t l, l', dn) - | Some pat -> (l, insert t l', Btermdn.add dn (pat,t)) + None -> if not (List.mem t l) then (insert t l, l', dn) else (l, l', dn) + | Some pat -> if not (List.mem t l') then (l, insert t l', Btermdn.add dn (pat,t)) else (l, l', dn) let lookup_tacs (hdc,c) (l,l',dn) = diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 6b322675c5..a54de8b8a7 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -1367,7 +1367,7 @@ let add_morphism_infer m n = let cst = Declare.declare_internal_constant instance_id (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) in - add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst }; + add_instance (Typeclasses.new_instance (Lazy.force morphism_class) None false cst); declare_projection n instance_id (ConstRef cst) else let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in @@ -1376,7 +1376,7 @@ let add_morphism_infer m n = Command.start_proof instance_id kind instance (fun _ -> function Libnames.ConstRef cst -> - add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst }; + add_instance (Typeclasses.new_instance (Lazy.force morphism_class) None false cst); declare_projection n instance_id (ConstRef cst) | _ -> assert false); Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) (); |