diff options
| author | Pierre-Marie Pédrot | 2017-09-05 00:35:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 00:36:04 +0200 |
| commit | ebe95a28cf012aff33eb5ce167be6520e6643cfd (patch) | |
| tree | 7899394e30ae4097936d4d4477c1f1ca48192466 /src | |
| parent | ada4c3aadb5c6b1870c2bf962ef9e1b07cc4bb05 (diff) | |
More static invariants for typeclass_eauto.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2stdlib.ml | 7 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 10 | ||||
| -rw-r--r-- | src/tac2tactics.mli | 4 |
3 files changed, 13 insertions, 8 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml index ed0e6aafd3..b64aac3559 100644 --- a/src/tac2stdlib.ml +++ b/src/tac2stdlib.ml @@ -665,10 +665,9 @@ let () = define_prim4 "tac_newauto" begin fun bt dbg n lems dbs -> Tac2tactics.new_auto dbg n lems dbs end -let () = define_prim4 "tac_typeclasses_eauto" begin fun bt b str n dbs -> - let b = Value.to_bool b in +let () = define_prim3 "tac_typeclasses_eauto" begin fun bt str n dbs -> let str = to_strategy str in let n = Value.to_option Value.to_int n in - let dbs = Value.to_list Value.to_ident dbs in - Tac2tactics.typeclasses_eauto b str n dbs + let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in + Tac2tactics.typeclasses_eauto str n dbs end diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index b35e26c89e..6cf8f24f27 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -243,6 +243,12 @@ let eauto debug n p lems dbs = let dbs = Option.map (fun l -> List.map Id.to_string l) dbs in Eauto.gen_eauto (Eauto.make_dimension n p) lems dbs -let typeclasses_eauto only_classes strategy depth dbs = - let dbs = List.map Id.to_string dbs in +let typeclasses_eauto strategy depth dbs = + let only_classes, dbs = match dbs with + | None -> + true, [Hints.typeclasses_db] + | Some dbs -> + let dbs = List.map Id.to_string dbs in + false, dbs + in Class_tactics.typeclasses_eauto ~only_classes ~strategy ~depth dbs diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli index 4369919d31..e0cd77096b 100644 --- a/src/tac2tactics.mli +++ b/src/tac2tactics.mli @@ -97,5 +97,5 @@ val new_auto : Hints.debug -> int option -> constr tactic list -> val eauto : Hints.debug -> int option -> int option -> constr tactic list -> Id.t list option -> unit Proofview.tactic -val typeclasses_eauto : bool -> Class_tactics.search_strategy -> int option -> - Id.t list -> unit Proofview.tactic +val typeclasses_eauto : Class_tactics.search_strategy -> int option -> + Id.t list option -> unit Proofview.tactic |