diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-05 21:32:11 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-05 21:32:11 +0000 |
| commit | 4a38c36307bf6333f6c26590820dfd82d643edf2 (patch) | |
| tree | 67902e5edfa95fc9b4025488545b07b876ef1fca /tactics/class_tactics.ml4 | |
| parent | 76cbb3b74c5611fb8c274d4c911d5c83f85351a7 (diff) | |
Minor fixes:
- Allow unicode superscripts characters.
- Put Program notations in scopes.
- Correct priority semantics in typeclasses eauto.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10759 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index c87baf25f..075077048 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -182,7 +182,7 @@ module SearchProblem = struct List.length (sig_it (fst s.tacres)) + nb_empty_evars (sig_sig (fst s.tacres)) in - if d <> 0 then d else + if d <> 0 && d <> 1 then d else let pri = s.pri - s'.pri in if pri <> 0 then pri else nbgoals s - nbgoals s' @@ -1027,7 +1027,7 @@ let require_library dirpath = let check_required_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in - if not (Library.library_is_opened dir) then + if not (Library.library_is_opened dir) || not (Library.library_is_loaded dir) then error ("Library "^(list_last d)^" has to be required first") let init_setoid () = |