diff options
| author | Cyril Cohen | 2015-07-22 15:33:35 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2015-07-22 15:33:35 +0200 |
| commit | f538fc0fb1ad454981e0ede5fb563919d5c95cf9 (patch) | |
| tree | 8aca276a60dea0cbe6509a6c5bb37312e5f56912 /mathcomp | |
| parent | ab387ba789820bc9115db5e0ae6ac29be7983e5b (diff) | |
blind patch by Enrico
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 index 0d9acdf..effd193 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 @@ -992,7 +992,8 @@ let interp_pattern ist gl red redty = aux [] (Evarutil.nf_evar sigma rp) in let sigma = List.fold_left (fun sigma e -> - if Evd.is_defined sigma e then sigma else (* clear may be recursiv *) + if Evd.is_defined sigma e then sigma else (* clear may be recursive *) + if Option.is_empty !to_clean then sigma else let name = Option.get !to_clean in pp(lazy(pr_id name)); try snd(Logic.prim_refiner (Proof_type.Thin [name]) sigma e) |