diff options
| author | msozeau | 2009-05-16 13:41:38 +0000 |
|---|---|---|
| committer | msozeau | 2009-05-16 13:41:38 +0000 |
| commit | b0e371b354ffdbf4a8572924602d04848020079e (patch) | |
| tree | 4f656ec0d438667e479d76d1ee22bb74e2cd0577 /tactics | |
| parent | 47c3ff53ee1c6b93172da74cc9916f0e9c51516d (diff) | |
Minor fixes in typeclasses:
- Set implicit args on for Context decls
- Move class_apply tactic to Init
- Normalize evars before raising an error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12127 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -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 e09ba93f8e..f9485e64cd 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -446,8 +446,8 @@ let resolve_all_evars debug m env p oevd do_split fail = | None -> if fail then (* Unable to satisfy the constraints. *) - let evm = evd in - let evm = if do_split then select_evars comp evm else evm in + let evm = if do_split then select_evars comp evd else evd in + let evm = Evarutil.nf_evars evm in let _, ev = Evd.fold (fun ev evi (b,acc) -> (* focus on one instance if only one was searched for *) |