blob: 3a2cee9f72924da70b6e4a5f0daa0c8b91c056f4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4deps: "grammar/grammar.cma" i*)
open Pp
open Genarg
open Tacexpr
DECLARE PLUGIN "g_auto"
(* Hint bases *)
let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
ARGUMENT EXTEND hintbases
TYPED AS preident_list_opt
PRINTED BY pr_hintbases
| [ "with" "*" ] -> [ None ]
| [ "with" ne_preident_list(l) ] -> [ Some l ]
| [ ] -> [ Some [] ]
END
let eval_uconstrs ist cs =
let flags = {
Pretyping.use_typeclasses = false;
use_unif_heuristics = true;
use_hook = Some Pfedit.solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true
} in
List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs
let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ())
ARGUMENT EXTEND auto_using
TYPED AS uconstr_list
PRINTED BY pr_auto_using
| [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ]
| [ ] -> [ [] ]
END
TACTIC EXTEND trivial
| [ "trivial" auto_using(lems) hintbases(db) ] ->
[ Auto.h_trivial (eval_uconstrs ist lems) db ]
END
TACTIC EXTEND info_trivial
| [ "info_trivial" auto_using(lems) hintbases(db) ] ->
[ Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db ]
END
TACTIC EXTEND debug_trivial
| [ "debug" "trivial" auto_using(lems) hintbases(db) ] ->
[ Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db ]
END
TACTIC EXTEND auto
| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
[ Auto.h_auto n (eval_uconstrs ist lems) db ]
END
TACTIC EXTEND info_auto
| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
[ Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db ]
END
TACTIC EXTEND debug_auto
| [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
[ Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db ]
END
|
