diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-04 12:37:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-04 12:37:05 +0000 |
| commit | 0fec4583628dfba57c4bbcf10e8c1fc053c5ec93 (patch) | |
| tree | 18018c90d6c3587d1b5d65d4e57ae32f0ef500de /tactics/hiddentac.mli | |
| parent | a42d753ac38896e58158311b3c384e80c9fd3fd4 (diff) | |
- Add more precise error localisation when one of the application fails
in a chain of apply or apply-in.
- Improved comments on the notions of permutation used in the library (still
the equality relation in file Permutation.v misses the property of being
effectively an equivalence relation, hence missing expected properties of
this notion of permutation).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12261 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index f5b2dbb55..6f592108b 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -38,9 +38,9 @@ val h_exact_no_check : constr -> tactic val h_vm_cast_no_check : constr -> tactic val h_apply : advanced_flag -> evars_flag -> - open_constr with_bindings list -> tactic + open_constr with_bindings located list -> tactic val h_apply_in : advanced_flag -> evars_flag -> - open_constr with_bindings list -> + open_constr with_bindings located list -> identifier * intro_pattern_expr located option -> tactic val h_elim : evars_flag -> constr with_ebindings -> |