diff options
| author | msozeau | 2008-03-06 14:56:08 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-06 14:56:08 +0000 |
| commit | 07ffd30a82ebfe35811ca43d71aeacdb86f4cc87 (patch) | |
| tree | 079a8c517c979db931d576d606a47e75627318c6 /tactics/auto.mli | |
| parent | 6f3400ed7f6aa2810d72f803273f04a7add04207 (diff) | |
Syntax changes in typeclasses, remove "?" for usual implicit arguments
binding, add "!" syntax for the new binders which require parameters and
not superclasses. Change backquotes for curly braces for user-given
implicit arguments, following tradition. This requires a hack a la
lpar-id-coloneq. Change ident to global for typeclass names in class
binders. Also requires a similar hack to distinguish between [ C t1 tn ]
and [ c : C t1 tn ]. Update affected theories.
While hacking the parsing of { wf }, factorized the two versions of fix
annotation parsing that were present in g_constr and g_vernac.
Add the possibility of the user optionaly giving the priority for resolve and
exact hints (used by type classes). Syntax not fixed yet: a natural
after the list of lemmas in "Hint Resolve" syntax, a natural after a "|"
after the instance constraint in Instance declarations (ex in
Morphisms.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index ac4f126f38..de3814630d 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -72,19 +72,19 @@ val print_hint_ref : global_reference -> unit val print_hint_db_by_name : hint_db_name -> unit -(* [make_exact_entry hint_name (c, ctyp)]. +(* [make_exact_entry pri (c, ctyp)]. [c] is the term given as an exact proof to solve the goal; - [ctyp] is the type of [hc]. *) + [ctyp] is the type of [c]. *) -val make_exact_entry : constr * constr -> global_reference * pri_auto_tactic +val make_exact_entry : int option -> constr * constr -> global_reference * pri_auto_tactic -(* [make_apply_entry (eapply,verbose) (c,cty)]. +(* [make_apply_entry (eapply,verbose) pri (c,cty)]. [eapply] is true if this hint will be used only with EApply; [c] is the term given as an exact proof to solve the goal; [cty] is the type of [hc]. *) val make_apply_entry : - env -> evar_map -> bool * bool -> constr * constr + env -> evar_map -> bool * bool -> int option -> constr * constr -> global_reference * pri_auto_tactic (* A constr which is Hint'ed will be: @@ -95,7 +95,7 @@ val make_apply_entry : has missing arguments. *) val make_resolves : - env -> evar_map -> bool -> constr -> + env -> evar_map -> bool -> int option -> constr -> (global_reference * pri_auto_tactic) list (* [make_resolve_hyp hname htyp]. |